Commit 2023-06-19 10:10 32106e95

View on Github →

feat: The lattice of complemented elements (#5194) Match https://github.com/leanprover-community/mathlib/pull/16267

Estimated changes

Modified Mathlib/Order/Disjoint.lean

added theorem Complementeds.codisjoint_coe

added theorem Complementeds.coe_bot

added theorem Complementeds.coe_inf

added theorem Complementeds.coe_inj

added theorem Complementeds.coe_injective

added theorem Complementeds.coe_le_coe

added theorem Complementeds.coe_lt_coe

added theorem Complementeds.coe_sup

added theorem Complementeds.coe_top

added theorem Complementeds.disjoint_coe

added theorem Complementeds.isCompl_coe

added theorem Complementeds.mk_bot

added theorem Complementeds.mk_inf_mk

added theorem Complementeds.mk_sup_mk

added theorem Complementeds.mk_top

added def Complementeds

added theorem IsComplemented.inf

added theorem IsComplemented.sup

added def IsComplemented

added theorem isComplemented_bot

added theorem isComplemented_top