no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
hg : LeftOrdContinuous g
hf : LeftOrdContinuous f
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (g ∘ f '' s) ((g ∘ f) x)
simpa only [image_image] using hg (hf h)