[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a b : α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
classical
  /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
        of `f` to the left of `x` for `x ≥ a`. -/
rcases hl with ⟨a, ha⟩
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x => hu.mono (image_subset _ (inter_subset_right _ _))
let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have hgs : EqOn f g s := by
  intro x hx
  simp only []
  have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
  rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
refine' ⟨g, fun x y hxy => _, hgs⟩
by_cases hx : Disjoint (Iic x) s <;> by_cases hy : Disjoint (Iic y) s <;>
  simp only [if_pos, if_neg, not_false_iff, *, refl]
· rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
  exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
· exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
· rw [not_disjoint_iff_nonempty_inter] at hx hy 
  refine' csSup_le_csSup (hu' _) (hx.image _) (image_subset _ _)
  exact inter_subset_inter_left _ (Iic_subset_Iic.2 hxy)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a b : α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
rcases hl with ⟨a, ha⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x => hu.mono (image_subset _ (inter_subset_right _ _))
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
have hgs : EqOn f g s := by
  intro x hx
  simp only []
  have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
  rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ EqOn f g s
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ f x = g x
[PROOFSTEP]
simp only []
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[PROOFSTEP]
have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[PROOFSTEP]
rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
refine' ⟨g, fun x y hxy => _, hgs⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hx : Disjoint (Iic x) s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hy : Disjoint (Iic y) s
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hy : Disjoint (Iic y) s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ a ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
z : α
hz : z ∈ Iic y ∩ s
⊢ a ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ a
[PROOFSTEP]
exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
rw [not_disjoint_iff_nonempty_inter] at hx hy 
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Set.Nonempty (Iic x ∩ s)
hy : Set.Nonempty (Iic y ∩ s)
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
refine' csSup_le_csSup (hu' _) (hx.image _) (image_subset _ _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Set.Nonempty (Iic x ∩ s)
hy : Set.Nonempty (Iic y ∩ s)
⊢ Iic x ∩ s ⊆ Iic y ∩ s
[PROOFSTEP]
exact inter_subset_inter_left _ (Iic_subset_Iic.2 hxy)
