Disjointness and complements #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines disjoint
, codisjoint
, and the is_compl
predicate.
Main declarations #
disjoint x y
: two elements of a lattice are disjoint if theirinf
is the bottom element.codisjoint x y
: two elements of a lattice are codisjoint if theirjoin
is the top element.is_compl x y
: In a bounded lattice, predicate for "x
is a complement ofy
". Note that in a non distributive lattice, an element can have several complements.complemented_lattice α
: Typeclass stating that any element of a lattice has a complement.
Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)
Note that we define this without reference to ⊓
, as this allows us to talk about orders where
the infimum is not unique, or where implementing has_inf
would require additional decidable
arguments.
Instances for disjoint
Alias of the forward direction of disjoint_self
.
Alias of the forward direction of codisjoint_self
.
- disjoint : disjoint x y
- codisjoint : codisjoint x y
Two elements x
and y
are complements of each other if x ⊔ y = ⊤
and x ⊓ y = ⊥
.
Instances for is_compl
A complemented bounded lattice is one where every element has a (not necessarily unique) complement.
Instances of this typeclass
- boolean_algebra.to_complemented_lattice
- complemented_lattice.order_dual.complemented_lattice
- is_modular_lattice.complemented_lattice_Iic
- is_modular_lattice.complemented_lattice_Ici
- module.submodule.complemented_lattice
- is_semisimple_module.is_semisimple_submodule
- monoid_algebra.submodule.complemented_lattice