Atoms, Coatoms, and Simple Lattices #
This module defines atoms, which are minimal non-⊥
elements in bounded lattices, simple lattices,
which are lattices with only two elements, and related ideas.
Main definitions #
Atoms and Coatoms #
is_atom a
indicates that the only element belowa
is⊥
.is_coatom a
indicates that the only element abovea
is⊤
.
Atomic and Atomistic Lattices #
is_atomic
indicates that every element other than⊥
is above an atom.is_coatomic
indicates that every element other than⊤
is below a coatom.is_atomistic
indicates that every element is theSup
of a set of atoms.is_coatomistic
indicates that every element is theInf
of a set of coatoms.
Simple Lattices #
is_simple_lattice
indicates that a bounded lattice has only two elements,⊥
and⊤
.is_simple_lattice.bounded_distrib_lattice
- Given an instance of
is_simple_lattice
, we provide the following definitions. These are not made global instances as they contain data :
Main results #
is_atom_dual_iff_is_coatom
andis_coatom_dual_iff_is_atom
express the (definitional) duality ofis_atom
andis_coatom
.is_simple_lattice_iff_is_atom_top
andis_simple_lattice_iff_is_coatom_bot
express the connection between atoms, coatoms, and simple latticesis_compl.is_atom_iff_is_coatom
andis_compl.is_coatom_if_is_atom
: In a modular bounded lattice, a complement of an atom is a coatom and vice versa.- ``is_atomic_iff_is_coatomic`: A modular complemented lattice is atomic iff it is coatomic.
A lattice is atomic iff every element other than ⊥
has an atom below it.
A lattice is coatomic iff every element other than ⊤
has a coatom above it.
A lattice is atomistic iff every element is a Sup
of a set of atoms.
A lattice is coatomistic iff every element is an Inf
of a set of coatoms.
A lattice is simple iff it has only two elements, ⊥
and ⊤
.
A simple bounded_lattice
is also distributive.
Equations
- is_simple_lattice.bounded_distrib_lattice = {sup := bounded_lattice.sup infer_instance, le := bounded_lattice.le infer_instance, lt := bounded_lattice.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf infer_instance, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := bounded_lattice.top infer_instance, le_top := _, bot := bounded_lattice.bot infer_instance, bot_le := _}
Every simple lattice is order-isomorphic to bool
.
A simple bounded_lattice
is also a boolean_algebra
.
Equations
- is_simple_lattice.boolean_algebra = {sup := bounded_distrib_lattice.sup is_simple_lattice.bounded_distrib_lattice, le := bounded_distrib_lattice.le is_simple_lattice.bounded_distrib_lattice, lt := bounded_distrib_lattice.lt is_simple_lattice.bounded_distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_distrib_lattice.inf is_simple_lattice.bounded_distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := bounded_distrib_lattice.top is_simple_lattice.bounded_distrib_lattice, le_top := _, bot := bounded_distrib_lattice.bot is_simple_lattice.bounded_distrib_lattice, bot_le := _, compl := λ (x : α), ite (x = ⊥) ⊤ ⊥, sdiff := λ (x y : α), ite (x = ⊤ ∧ y = ⊥) ⊤ ⊥, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}
A simple bounded_lattice
is also complete.
Equations
- is_simple_lattice.complete_lattice = {sup := bounded_lattice.sup infer_instance, le := bounded_lattice.le infer_instance, lt := bounded_lattice.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf infer_instance, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top infer_instance, le_top := _, bot := bounded_lattice.bot infer_instance, bot_le := _, Sup := λ (s : set α), ite (⊤ ∈ s) ⊤ ⊥, Inf := λ (s : set α), ite (⊥ ∈ s) ⊥ ⊤, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
A simple bounded_lattice
is also a complete_boolean_algebra
.
Equations
- is_simple_lattice.complete_boolean_algebra = {sup := complete_lattice.sup is_simple_lattice.complete_lattice, le := complete_lattice.le is_simple_lattice.complete_lattice, lt := complete_lattice.lt is_simple_lattice.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf is_simple_lattice.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := complete_lattice.top is_simple_lattice.complete_lattice, le_top := _, bot := complete_lattice.bot is_simple_lattice.complete_lattice, bot_le := _, compl := boolean_algebra.compl is_simple_lattice.boolean_algebra, sdiff := boolean_algebra.sdiff is_simple_lattice.boolean_algebra, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _, Sup := complete_lattice.Sup is_simple_lattice.complete_lattice, Inf := complete_lattice.Inf is_simple_lattice.complete_lattice, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, infi_sup_le_sup_Inf := _, inf_Sup_le_supr_inf := _}