F : Type ?u.114656
α : Type u_1
β : Type u_2
γ : Type ?u.114665
δ : Type ?u.114668
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ↑f ⊤ ≤ ↑f (a ⊔ b)
F : Type ?u.114656
α : Type u_1
β : Type u_2
γ : Type ?u.114665
δ : Type ?u.114668
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (↑f a) (↑f b)
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
no goals
F : Type ?u.114656
α : Type u_1
β : Type u_2
γ : Type ?u.114665
δ : Type ?u.114668
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ↑f ⊤ ≤ ↑f (a ⊔ b)
exact f.monotone ha.top_le