[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a✝ b : α
s : Finset β
hs : Finset.Nonempty s
f : β → α
a : α
⊢ sup' s hs f ≤ a ↔ sSup (f '' ↑s) ≤ a
[PROOFSTEP]
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (hs.to_set.image f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup' s hs id = sSup ↑s
[PROOFSTEP]
rw [hs.sup'_eq_cSup_image, Set.image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ sSup ↑s ∈ s
[PROOFSTEP]
rw [h.cSup_eq_max']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ max' s h ∈ s
[PROOFSTEP]
exact s.max'_mem _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
h : Set.Nonempty s
hs : Set.Finite s
⊢ sSup s ∈ s
[PROOFSTEP]
lift s to Finset α using hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
a b : α
s : Finset α
h : Set.Nonempty ↑s
⊢ sSup ↑s ∈ ↑s
[PROOFSTEP]
exact Finset.Nonempty.cSup_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f = sSup (f '' ↑s)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f ≤ sSup (f '' ↑s)
[PROOFSTEP]
refine' Finset.sup'_le _ _ fun a ha => _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ f a ≤ sSup (f '' ↑s)
[PROOFSTEP]
refine' le_csSup ⟨s.sup' H f, _⟩ ⟨a, ha, rfl⟩
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ sup' s H f ∈ upperBounds (f '' ↑s)
[PROOFSTEP]
rintro i ⟨j, hj, rfl⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
j : α
hj : j ∈ ↑s
⊢ f j ≤ sup' s H f
[PROOFSTEP]
exact Finset.le_sup' _ hj
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sSup (f '' ↑s) ≤ sup' s H f
[PROOFSTEP]
apply csSup_le ((coe_nonempty.mpr H).image _)
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ ∀ (b : β), b ∈ f '' ↑s → b ≤ sup' s H f
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ ↑s
⊢ f a ≤ sup' s H f
[PROOFSTEP]
exact Finset.le_sup' _ ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s : Finset α
H : Finset.Nonempty s
⊢ sup' s H id = sSup ↑s
[PROOFSTEP]
rw [sup'_eq_csSup_image s H, Set.image_id]
