Commit 2023-10-06 12:22 e2c210a9

View on Github →

feat: add lemmas Disjoint.isCompl_sup_right_of_isCompl_sup_left (and partner) (#7483)

Estimated changes

Modified Mathlib/Order/ModularLattice.lean

modified theorem Disjoint.disjoint_sup_left_of_disjoint_sup_right

modified theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left

added theorem Disjoint.isCompl_sup_left_of_isCompl_sup_right

added theorem Disjoint.isCompl_sup_right_of_isCompl_sup_left