no goals
α : Type u_1
β : Type u_2
γ : Type ?u.28103
δ : Type ?u.28106
ι : Sort ?u.28109
κ : ι → Sort ?u.28114
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s t : Interval α
a b : α
f : α →o β
⊢ ↑f '' ↑⊥ ⊆ ↑(map f ⊥)
simp