Theorem Disjoint.isCompl_sup_left_of_isCompl_sup_right

Modification history

2023-10-07 06:50
Mathlib/Order/ModularLattice.lean
chore: relax typeclass assumptions in two modular lattice lemmas (#7555)
Modified Disjoint.isCompl_sup_left_of_isCompl_sup_rightView on Github →
2023-10-06 12:22
Mathlib/Order/ModularLattice.lean
feat: add lemmas `Disjoint.isCompl_sup_right_of_isCompl_sup_left` (and partner) (#7483)
Added Disjoint.isCompl_sup_left_of_isCompl_sup_rightView on Github →