Disjointness and complements #
This file defines Disjoint
, Codisjoint
, and the IsCompl
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.IsCompl 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.ComplementedLattice α
: 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 Inf
would require additional Decidable
arguments.
Alias of the forward direction of disjoint_self
.
Alias of the forward direction of codisjoint_self
.
If
x
andy
are to be complementary in an order, they should be disjoint.Disjoint : Disjoint x yIf
x
andy
are to be complementary in an order, they should be codisjoint.Codisjoint : Codisjoint x y
Two elements x
and y
are complements of each other if x ⊔ y = ⊤⊔ y = ⊤⊤
and x ⊓ y = ⊥⊓ y = ⊥⊥
.
Instances For
In a
ComplementedLattice
, every element admits a complement.exists_isCompl : ∀ (a : α), ∃ b, IsCompl a b
A complemented bounded lattice is one where every element has a (not necessarily unique) complement.
Instances
Equations
- One or more equations did not get rendered due to their size.