# Documentation

Mathlib.Order.Atoms

# 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 #

• IsAtom a indicates that the only element below a is ⊥.
• IsCoatom a indicates that the only element above a is ⊤.

### Atomic and Atomistic Lattices #

• IsAtomic indicates that every element other than ⊥ is above an atom.
• IsCoatomic indicates that every element other than ⊤ is below a coatom.
• IsAtomistic indicates that every element is the supₛ of a set of atoms.
• IsCoatomistic indicates that every element is the infₛ of a set of coatoms.

### Simple Lattices #

• IsSimpleOrder indicates that an order has only two unique elements, ⊥ and ⊤.
• IsSimpleOrder.boundedOrder
• IsSimpleOrder.distribLattice
• Given an instance of IsSimpleOrder, we provide the following definitions. These are not made global instances as they contain data :
• IsSimpleOrder.booleanAlgebra
• IsSimpleOrder.completeLattice
• IsSimpleOrder.completeBooleanAlgebra

## Main results #

• isAtom_dual_iff_isCoatom and isCoatom_dual_iff_isAtom express the (definitional) duality of IsAtom and IsCoatom.
• isSimpleOrder_iff_isAtom_top and isSimpleOrder_iff_isCoatom_bot express the connection between atoms, coatoms, and simple lattices
• IsCompl.isAtom_iff_isCoatom and IsCompl.isCoatom_if_isAtom: In a modular bounded lattice, a complement of an atom is a coatom and vice versa.
• isAtomic_iff_isCoatomic: A modular complemented lattice is atomic iff it is coatomic.
def IsAtom {α : Type u_1} [inst : ] [inst : ] (a : α) :

An atom of an OrderBot is an element with no other element between it and ⊥, which is not ⊥.

Equations
theorem IsAtom.Iic {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (ha : ) (hax : a x) :
IsAtom { val := a, property := hax }
theorem IsAtom.of_isAtom_coe_Iic {α : Type u_1} [inst : ] [inst : ] {x : α} {a : ↑()} (ha : ) :
IsAtom a
theorem isAtom_iff {α : Type u_1} [inst : ] [inst : ] {a : α} :
a ∀ (b : α), b b aa b
theorem IsAtom.lt_iff {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (h : ) :
x < a x =
theorem IsAtom.le_iff {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (h : ) :
x a x = x = a
theorem IsAtom.Iic_eq {α : Type u_1} [inst : ] [inst : ] {a : α} (h : ) :
= {, a}
@[simp]
theorem bot_covby_iff {α : Type u_1} [inst : ] [inst : ] {a : α} :
theorem Covby.is_atom {α : Type u_1} [inst : ] [inst : ] {a : α} :
a

Alias of the forward direction of bot_covby_iff.

theorem IsAtom.bot_covby {α : Type u_1} [inst : ] [inst : ] {a : α} :
a

Alias of the reverse direction of bot_covby_iff.

def IsCoatom {α : Type u_1} [inst : ] [inst : ] (a : α) :

A coatom of an OrderTop is an element with no other element between it and ⊤, which is not ⊤.

Equations
@[simp]
theorem isCoatom_dual_iff_isAtom {α : Type u_1} [inst : ] [inst : ] {a : α} :
IsCoatom (OrderDual.toDual a)
@[simp]
theorem isAtom_dual_iff_isCoatom {α : Type u_1} [inst : ] [inst : ] {a : α} :
IsAtom (OrderDual.toDual a)
theorem IsAtom.dual {α : Type u_1} [inst : ] [inst : ] {a : α} :
IsCoatom (OrderDual.toDual a)

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

theorem IsCoatom.dual {α : Type u_1} [inst : ] [inst : ] {a : α} :
IsAtom (OrderDual.toDual a)

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

theorem IsCoatom.Ici {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (ha : ) (hax : x a) :
IsCoatom { val := a, property := hax }
theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_1} [inst : ] [inst : ] {x : α} {a : ↑()} (ha : ) :
theorem isCoatom_iff {α : Type u_1} [inst : ] [inst : ] {a : α} :
a ∀ (b : α), b a bb a
theorem IsCoatom.lt_iff {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (h : ) :
a < x x =
theorem IsCoatom.le_iff {α : Type u_1} [inst : ] [inst : ] {a : α} {x : α} (h : ) :
a x x = x = a
theorem IsCoatom.Ici_eq {α : Type u_1} [inst : ] [inst : ] {a : α} (h : ) :
= {, a}
@[simp]
theorem covby_top_iff {α : Type u_1} [inst : ] [inst : ] {a : α} :
theorem Covby.is_coatom {α : Type u_1} [inst : ] [inst : ] {a : α} :
a

Alias of the forward direction of covby_top_iff.

theorem IsCoatom.covby_top {α : Type u_1} [inst : ] [inst : ] {a : α} :
a

Alias of the reverse direction of covby_top_iff.

@[simp]
theorem Set.Ici.isAtom_iff {α : Type u_1} [inst : ] {a : α} {b : ↑()} :
a b
@[simp]
theorem Set.Iic.isCoatom_iff {α : Type u_1} [inst : ] {b : α} {a : ↑()} :
a b
theorem covby_iff_atom_Ici {α : Type u_1} [inst : ] {a : α} {b : α} (h : a b) :
a b IsAtom { val := b, property := h }
theorem covby_iff_coatom_Iic {α : Type u_1} [inst : ] {a : α} {b : α} (h : a b) :
a b IsCoatom { val := a, property := h }
theorem IsAtom.inf_eq_bot_of_ne {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
a b =
theorem IsAtom.disjoint_of_ne {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
theorem IsCoatom.sup_eq_top_of_ne {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
a b =
theorem IsAtomic_iff (α : Type u_1) [inst : ] [inst : ] :
∀ (b : α), b = a, a b
class IsAtomic (α : Type u_1) [inst : ] [inst : ] :
• Every element other than ⊥ has an atom below it.

eq_bot_or_exists_atom_le : ∀ (b : α), b = a, a b

A lattice is atomic iff every element other than ⊥ has an atom below it.

Instances
theorem IsCoatomic_iff (α : Type u_1) [inst : ] [inst : ] :
∀ (b : α), b = a, b a
class IsCoatomic (α : Type u_1) [inst : ] [inst : ] :
• Every element other than ⊤ has an atom above it.

eq_top_or_exists_le_coatom : ∀ (b : α), b = a, b a

A lattice is coatomic iff every element other than ⊤ has a coatom above it.

Instances
@[simp]
theorem isCoatomic_dual_iff_isAtomic {α : Type u_1} [inst : ] [inst : ] :
@[simp]
theorem isAtomic_dual_iff_isCoatomic {α : Type u_1} [inst : ] [inst : ] :
instance IsAtomic.isCoatomic_dual {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
instance IsAtomic.Set.Iic.isAtomic {α : Type u_1} [inst : ] [inst : ] [inst : ] {x : α} :
IsAtomic ↑()
Equations
instance IsCoatomic.isCoatomic {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_1} [inst : ] [inst : ] [inst : ] {x : α} :
Equations
theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_1} [inst : ] [inst : ] :
∀ (x : α), IsAtomic ↑()
theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_1} [inst : ] [inst : ] :
∀ (x : α), IsCoatomic ↑()
theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [inst : ] [inst : ] (h : WellFounded fun x x_1 => x < x_1) :
theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [inst : ] [inst : ] (h : WellFounded fun x x_1 => x > x_1) :
class IsAtomistic (α : Type u_1) [inst : ] :
• Every element is a supₛ of a set of atoms.

eq_supₛ_atoms : ∀ (b : α), s, b = supₛ s ∀ (a : α), a s

A lattice is atomistic iff every element is a supₛ of a set of atoms.

Instances
class IsCoatomistic (α : Type u_1) [inst : ] :
• Every element is a infₛ of a set of coatoms.

eq_infₛ_coatoms : ∀ (b : α), s, b = infₛ s ∀ (a : α), a s

A lattice is coatomistic iff every element is an infₛ of a set of coatoms.

Instances
@[simp]
theorem isCoatomistic_dual_iff_isAtomistic {α : Type u_1} [inst : ] :
@[simp]
theorem isAtomistic_dual_iff_isCoatomistic {α : Type u_1} [inst : ] :
instance IsAtomistic.isCoatomistic_dual {α : Type u_1} [inst : ] [h : ] :
Equations
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem supₛ_atoms_le_eq {α : Type u_1} [inst : ] [inst : ] (b : α) :
supₛ { a | a b } = b
@[simp]
theorem supₛ_atoms_eq_top {α : Type u_1} [inst : ] [inst : ] :
supₛ { a | } =
theorem le_iff_atom_le_imp {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} :
a b ∀ (c : α), c ac b
instance IsCoatomistic.isAtomistic_dual {α : Type u_1} [inst : ] [h : ] :
Equations
Equations
• One or more equations did not get rendered due to their size.
class IsSimpleOrder (α : Type u_1) [inst : LE α] [inst : ] extends :
• Every element is either ⊥ or ⊤

eq_bot_or_eq_top : ∀ (a : α), a = a =

An order is simple iff it has exactly two elements, ⊥ and ⊤.

Instances
theorem isSimpleOrder_iff_isSimpleOrder_orderDual {α : Type u_1} [inst : LE α] [inst : ] :
theorem IsSimpleOrder.bot_ne_top {α : Type u_1} [inst : LE α] [inst : ] [inst : ] :
instance instIsSimpleOrderOrderDualInstLEOrderDualBoundedOrder {α : Type u_1} [inst : LE α] [inst : ] [inst : ] :
Equations
def IsSimpleOrder.preorder {α : Type u_1} [inst : LE α] [inst : ] [inst : ] :

A simple BoundedOrder induces a preorder. This is not an instance to prevent loops.

Equations
• IsSimpleOrder.preorder = Preorder.mk (_ : ∀ (a : α), a a) (_ : ∀ (a b c : α), a bb ca c)
def IsSimpleOrder.linearOrder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :

A simple partial ordered BoundedOrder induces a linear order. This is not an instance to prevent loops.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem isAtom_top {α : Type u_1} [inst : ] [inst : ] [inst : ] :
@[simp]
theorem isCoatom_bot {α : Type u_1} [inst : ] [inst : ] [inst : ] :
theorem bot_covby_top {α : Type u_1} [inst : ] [inst : ] [inst : ] :
theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (h : a < b) :
a =
theorem IsSimpleOrder.eq_top_of_lt {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (h : a < b) :
b =
theorem IsSimpleOrder.LT.lt.eq_bot {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (h : a < b) :
a =

Alias of IsSimpleOrder.eq_bot_of_lt.

theorem IsSimpleOrder.LT.lt.eq_top {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (h : a < b) :
b =

Alias of IsSimpleOrder.eq_top_of_lt.

def IsSimpleOrder.lattice {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :

A simple partial ordered BoundedOrder induces a lattice. This is not an instance to prevent loops

Equations
• IsSimpleOrder.lattice = LinearOrder.toLattice
def IsSimpleOrder.distribLattice {α : Type u_1} [inst : ] [inst : ] [inst : ] :

A lattice that is a BoundedOrder is a distributive lattice. This is not an instance to prevent loops

Equations
Equations
@[simp]
theorem IsSimpleOrder.equivBool_apply {α : Type u_1} [inst : ] [inst : LE α] [inst : ] [inst : ] (x : α) :
IsSimpleOrder.equivBool x = decide (x = )
@[simp]
theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_1} [inst : ] [inst : LE α] [inst : ] [inst : ] (x : Bool) :
↑(Equiv.symm IsSimpleOrder.equivBool) x = bif x then else
def IsSimpleOrder.equivBool {α : Type u_1} [inst : ] [inst : LE α] [inst : ] [inst : ] :

Every simple lattice is isomorphic to Bool, regardless of order.

Equations
• One or more equations did not get rendered due to their size.
def IsSimpleOrder.orderIsoBool {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :

Every simple lattice over a partial order is order-isomorphic to Bool.

Equations
• One or more equations did not get rendered due to their size.
def IsSimpleOrder.booleanAlgebra {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :

A simple BoundedOrder is also a BooleanAlgebra.

Equations
• One or more equations did not get rendered due to their size.
noncomputable def IsSimpleOrder.completeLattice {α : Type u_1} [inst : ] [inst : ] [inst : ] :

A simple BoundedOrder is also complete.

Equations
• One or more equations did not get rendered due to their size.
noncomputable def IsSimpleOrder.completeBooleanAlgebra {α : Type u_1} [inst : ] [inst : ] [inst : ] :

A simple BoundedOrder is also a CompleteBooleanAlgebra.

Equations
• One or more equations did not get rendered due to their size.
instance IsSimpleOrder.instIsAtomistic {α : Type u_1} [inst : ] [inst : ] :
Equations
instance IsSimpleOrder.instIsCoatomistic {α : Type u_1} [inst : ] [inst : ] :
Equations
theorem isSimpleOrder_iff_isAtom_top {α : Type u_1} [inst : ] [inst : ] :
theorem isSimpleOrder_iff_isCoatom_bot {α : Type u_1} [inst : ] [inst : ] :
theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_1} [inst : ] [inst : ] {a : α} :
theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_1} [inst : ] [inst : ] {a : α} :
theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : β ↪o α) (hbot : f.toEmbedding = ) {b : β} (hb : IsAtom (f.toEmbedding b)) :
theorem OrderEmbedding.isCoatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : β ↪o α) (htop : f.toEmbedding = ) {b : β} (hb : IsCoatom (f.toEmbedding b)) :
theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (hbot : u = ) {b : β} (hb : IsAtom (u b)) :
theorem GaloisInsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (hbot : u = ) (h_atom : ∀ (a : α), u (l a) = a) (a : α) :
IsAtom (l a)
theorem GaloisInsertion.isAtom_iff' {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (hbot : u = ) (h_atom : ∀ (a : α), u (l a) = a) (b : β) :
IsAtom (u b)
theorem GaloisInsertion.isCoatom_of_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) {b : β} (hb : IsCoatom (u b)) :
theorem GaloisInsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (h_coatom : ∀ (a : α), u (l a) = a) (b : β) :
IsCoatom (u b)
theorem GaloisCoinsertion.isCoatom_of_l_top {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (hbot : l = ) {a : α} (hb : IsCoatom (l a)) :
theorem GaloisCoinsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (htop : l = ) (h_coatom : ∀ (b : β), l (u b) = b) (b : β) :
IsCoatom (u b)
theorem GaloisCoinsertion.isCoatom_iff' {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (htop : l = ) (h_coatom : ∀ (b : β), l (u b) = b) (a : α) :
IsCoatom (l a)
theorem GaloisCoinsertion.isAtom_of_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) {a : α} (hb : IsAtom (l a)) :
theorem GaloisCoinsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {l : αβ} {u : βα} (gi : ) (h_atom : ∀ (b : β), l (u b) = b) (a : α) :
IsAtom (l a)
@[simp]
theorem OrderIso.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : α ≃o β) (a : α) :
IsAtom (().toEmbedding a)
@[simp]
theorem OrderIso.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : α ≃o β) (a : α) :
IsCoatom (().toEmbedding a)
theorem OrderIso.isSimpleOrder_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : α ≃o β) :
theorem OrderIso.isSimpleOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [h : ] (f : α ≃o β) :
theorem OrderIso.isAtomic_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : α ≃o β) :
theorem OrderIso.isCoatomic_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : α ≃o β) :
theorem IsCompl.isAtom_iff_isCoatom {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (hc : IsCompl a b) :
theorem IsCompl.isCoatom_iff_isAtom {α : Type u_1} [inst : ] [inst : ] [inst : ] {a : α} {b : α} (hc : IsCompl a b) :
theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] :
theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] :
theorem isAtomic_iff_isCoatomic {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
theorem Set.isAtom_singleton {α : Type u_1} (x : α) :
IsAtom {x}
theorem Set.isAtom_iff {α : Type u_1} (s : Set α) :
x, s = {x}
theorem Set.isCoatom_iff {α : Type u_1} (s : Set α) :
x, s = {x}
theorem Set.isCoatom_singleton_compl {α : Type u_1} (x : α) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.