case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f ≤ sSup (f '' ↑s)

case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sSup (f '' ↑s) ≤ sup' s H f
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f = sSup (f '' ↑s)
apply le_antisymm
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ f a ≤ sSup (f '' ↑s)
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f ≤ sSup (f '' ↑s)
refine' Finset.sup'_le _ _ fun a ha => _
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ sup' s H f ∈ upperBounds (f '' ↑s)
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ f a ≤ sSup (f '' ↑s)
refine' le_csSup ⟨s.sup' H f, _⟩ ⟨a, ha, rfl⟩
case a.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
j : α
hj : j ∈ ↑s
⊢ f j ≤ sup' s H f
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ sup' s H f ∈ upperBounds (f '' ↑s)
rintro i ⟨j, hj, rfl⟩
no goals
case a.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
j : α
hj : j ∈ ↑s
⊢ f j ≤ sup' s H f
exact Finset.le_sup' _ hj
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ ∀ (b : β), b ∈ f '' ↑s → b ≤ sup' s H f
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sSup (f '' ↑s) ≤ sup' s H f
apply csSup_le ((coe_nonempty.mpr H).image _)
case a.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ ↑s
⊢ f a ≤ sup' s H f
case a
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ ∀ (b : β), b ∈ f '' ↑s → b ≤ sup' s H f
rintro _ ⟨a, ha, rfl⟩
no goals
case a.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.12263
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ ↑s
⊢ f a ≤ sup' s H f
exact Finset.le_sup' _ ha