α : Type u_2
β : Type u_1
γ : Type ?u.31436
ι : Sort ?u.31439
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : Set.Nonempty s
⊢ IsLUB (f '' s) (sSup (f '' s))
α : Type u_2
β : Type u_1
γ : Type ?u.31436
ι : Sort ?u.31439
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : Set.Nonempty s
⊢ IsLUB (f '' s) (⨆ (i : ↑s), f ↑i)
rw [← sSup_image']
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.31436
ι : Sort ?u.31439
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : Set.Nonempty s
⊢ IsLUB (f '' s) (sSup (f '' s))
exact isLUB_csSup (Hne.image _) H