no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
⊢ f (sSup s) = ⨆ (x : α) (_ : x ∈ s), f x
rw [hf.map_sSup', sSup_image]