Theorem Disjoint.disjoint_sup_left_of_disjoint_sup_right

Modification history

2023-10-06 12:22
Mathlib/Order/ModularLattice.lean
feat: add lemmas `Disjoint.isCompl_sup_right_of_isCompl_sup_left` (and partner) (#7483)
Modified Disjoint.disjoint_sup_left_of_disjoint_sup_rightView on Github →
2022-12-29 11:06
Mathlib/Order/ModularLattice.lean
feat: port Order.ModularLattice (#1234)
Added Disjoint.disjoint_sup_left_of_disjoint_sup_rightView on Github →