[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ ¬y ≤ x
[PROOFSTEP]
simp [BddAbove, upperBounds, Set.Nonempty]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
a b : α✝
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ x < y
[PROOFSTEP]
simp only [not_bddAbove_iff', not_le]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s
[PROOFSTEP]
rw [h.upperBounds_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ lowerBounds s
[PROOFSTEP]
rw [h.lowerBounds_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t✝ : Set α
a✝ b a : α
s t : Set α
⊢ IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
[PROOFSTEP]
simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)
[PROOFSTEP]
rintro ⟨bs, hs⟩ ⟨bt, ht⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ BddAbove (s ∪ t)
[PROOFSTEP]
use bs ⊔ bt
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds (s ∪ t)
[PROOFSTEP]
rw [upperBounds_union]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds s ∩ upperBounds t
[PROOFSTEP]
exact ⟨upperBounds_mono_mem le_sup_left hs, upperBounds_mono_mem le_sup_right ht⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
h : a ≤ b
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
h : b ≤ a
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x
[PROOFSTEP]
rw [bddAbove_def, exists_ge_and_iff_exists]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ (y : γ), y ∈ s → y ≤ x
[PROOFSTEP]
exact Monotone.ball fun x _ => monotone_le
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
cases' eq_or_lt_of_le (lub_Iio_le i hj) with hj_eq_i hj_lt_i
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
exact Or.inl hj_eq_i
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
right
[GOAL]
case inr.h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j
[PROOFSTEP]
exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
refine' ⟨i, fun j hj => le_of_lt hj, _⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))
[PROOFSTEP]
rw [mem_lowerBounds]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
[PROOFSTEP]
by_contra h
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ False
[PROOFSTEP]
refine' h_exists_lt _
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ∃ x, x ∈ upperBounds (Iio i) ∧ x < i
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a
[PROOFSTEP]
cases' eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ h₂
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
exact h₁.symm ▸ le_sup_left
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
obtain ⟨y, lty, ylt⟩ := exists_between h₂
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b
[PROOFSTEP]
obtain ⟨u, au, ub⟩ := exists_between h
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b
[PROOFSTEP]
apply (hx ⟨au, ub⟩).trans ub.le
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ioo a b) b
[PROOFSTEP]
simpa only [dual_Ioo] using isGLB_Ioo hab.dual
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ico a b) b
[PROOFSTEP]
simpa only [dual_Ioc] using isGLB_Ioc hab.dual
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b
[PROOFSTEP]
simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici, bddAbove_iff_subset_Iic, exists_and_left,
  exists_and_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ IsGreatest univ a ↔ IsTop a
[PROOFSTEP]
simp [IsGreatest, mem_upperBounds, IsTop]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a b : α
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}
[PROOFSTEP]
rw [isGreatest_univ.upperBounds_eq, Ici_top]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMaxOrder α
⊢ ¬BddAbove univ
[PROOFSTEP]
simp [BddAbove]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ upperBounds ∅ = univ
[PROOFSTEP]
simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, ball_empty_iff, forall_true_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : Nonempty α
⊢ BddAbove ∅
[PROOFSTEP]
simp only [BddAbove, upperBounds_empty, univ_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : Nonempty α
⊢ BddBelow ∅
[PROOFSTEP]
simp only [BddBelow, lowerBounds_empty, univ_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ IsGLB ∅ a ↔ IsTop a
[PROOFSTEP]
simp [IsGLB]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ upperBounds s
[PROOFSTEP]
rw [h, upperBounds_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b : α
inst✝ : SemilatticeSup γ
a : γ
s : Set γ
⊢ BddAbove (insert a s) ↔ BddAbove s
[PROOFSTEP]
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b : α
inst✝ : SemilatticeInf γ
a : γ
s : Set γ
⊢ BddBelow (insert a s) ↔ BddBelow s
[PROOFSTEP]
simp only [insert_eq, bddBelow_union, bddBelow_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)
[PROOFSTEP]
exact isLUB_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB (insert a s) (a ⊓ b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB ({a} ∪ s) (a ⊓ b)
[PROOFSTEP]
exact isGLB_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (max a b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)
[PROOFSTEP]
exact isGreatest_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast (insert a s) (min a b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast ({a} ∪ s) (min a b)
[PROOFSTEP]
exact isLeast_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
a✝ b a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
[PROOFSTEP]
rw [insert_eq, upperBounds_union, upperBounds_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
a✝ b a : α
s : Set α
⊢ lowerBounds (insert a s) = Iic a ∩ lowerBounds s
[PROOFSTEP]
rw [insert_eq, lowerBounds_union, lowerBounds_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c, c ∈ s ∧ b < c
[PROOFSTEP]
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a : α
Hst✝ Hst : s ⊆ t
⊢ f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a✝ : α
Hst✝ Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)
[PROOFSTEP]
exact Hf.mem_upperBounds_image Hst ha.1 ha.2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
a : α
s : Set α
⊢ f '' upperBounds s ⊆ upperBounds (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
a✝ : α
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)
[PROOFSTEP]
exact Hf.mem_upperBounds_image ha
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2 h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2 h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
[PROOFSTEP]
simp only [bddAbove_pi, ← range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)
[PROOFSTEP]
classical
refine' ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => _⟩, fun H => ⟨_, _⟩⟩
· suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a
  refine' fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
· exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
· exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)
[PROOFSTEP]
refine' ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => _⟩, fun H => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b
[PROOFSTEP]
suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s
[PROOFSTEP]
refine' fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s
[PROOFSTEP]
exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)
[PROOFSTEP]
exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
[PROOFSTEP]
refine'
  ⟨fun H =>
    ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => _⟩, ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => _⟩⟩,
    fun H => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.fst ≤ a
[PROOFSTEP]
suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.snd) ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.snd ≤ a
[PROOFSTEP]
suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.fst, a) ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
[GOAL]
case refine'_4
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ lowerBounds (upperBounds s)
[PROOFSTEP]
exact fun q hq => ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq, H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
