F : Type ?u.113997
α : Type u_1
β : Type u_2
γ : Type ?u.114006
δ : Type ?u.114009
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ ↑f (a ⊓ b) ≤ ↑f ⊥
F : Type ?u.113997
α : Type u_1
β : Type u_2
γ : Type ?u.114006
δ : Type ?u.114009
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (↑f a) (↑f b)
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
no goals
F : Type ?u.113997
α : Type u_1
β : Type u_2
γ : Type ?u.114006
δ : Type ?u.114009
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ ↑f (a ⊓ b) ≤ ↑f ⊥
exact f.monotone ha.le_bot