α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c
rw [disjoint_comm, sup_comm]
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)
apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
no goals
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
a b c : α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
rwa [sup_comm, disjoint_comm] at hsup