# 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 sSup of a set of atoms.
• IsCoatomistic indicates that every element is the sInf 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} [] [] (a : α) :

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

Equations
Instances For
theorem IsAtom.Iic {α : Type u_1} [] [] {a : α} {x : α} (ha : ) (hax : a x) :
IsAtom a, hax
theorem IsAtom.of_isAtom_coe_Iic {α : Type u_1} [] [] {x : α} {a : ()} (ha : ) :
IsAtom a
theorem isAtom_iff_le_of_ge {α : Type u_1} [] [] {a : α} :
a ∀ (b : α), b b aa b
theorem IsAtom.lt_iff {α : Type u_1} [] [] {a : α} {x : α} (h : ) :
x < a x =
theorem IsAtom.le_iff {α : Type u_1} [] [] {a : α} {x : α} (h : ) :
x a x = x = a
theorem IsAtom.le_iff_eq {α : Type u_1} [] [] {a : α} {b : α} (ha : ) (hb : b ) :
b a b = a
theorem IsAtom.Iic_eq {α : Type u_1} [] [] {a : α} (h : ) :
= {, a}
@[simp]
theorem bot_covBy_iff {α : Type u_1} [] [] {a : α} :
theorem CovBy.is_atom {α : Type u_1} [] [] {a : α} :
a

Alias of the forward direction of bot_covBy_iff.

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

Alias of the reverse direction of bot_covBy_iff.

theorem atom_le_iSup {α : Type u_1} {a : α} {ι : Sort u_3} [] (ha : ) {f : ια} :
a iSup f ∃ (i : ι), a f i
def IsCoatom {α : Type u_1} [] [] (a : α) :

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

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

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

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

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

theorem IsCoatom.Ici {α : Type u_1} [] [] {a : α} {x : α} (ha : ) (hax : x a) :
IsCoatom a, hax
theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_1} [] [] {x : α} {a : ()} (ha : ) :
theorem isCoatom_iff_ge_of_le {α : Type u_1} [] [] {a : α} :
a ∀ (b : α), b a bb a
theorem IsCoatom.lt_iff {α : Type u_1} [] [] {a : α} {x : α} (h : ) :
a < x x =
theorem IsCoatom.le_iff {α : Type u_1} [] [] {a : α} {x : α} (h : ) :
a x x = x = a
theorem IsCoatom.le_iff_eq {α : Type u_1} [] [] {a : α} {b : α} (ha : ) (hb : b ) :
a b b = a
theorem IsCoatom.Ici_eq {α : Type u_1} [] [] {a : α} (h : ) :
= {, a}
@[simp]
theorem covBy_top_iff {α : Type u_1} [] [] {a : α} :
theorem IsCoatom.covBy_top {α : Type u_1} [] [] {a : α} :
a

Alias of the reverse direction of covBy_top_iff.

theorem CovBy.isCoatom {α : Type u_1} [] [] {a : α} :
a

Alias of the forward direction of covBy_top_iff.

theorem iInf_le_coatom {α : Type u_1} {a : α} {ι : Sort u_3} [] (ha : ) {f : ια} :
iInf f a ∃ (i : ι), f i a
@[simp]
theorem Set.Ici.isAtom_iff {α : Type u_1} [] {a : α} {b : ()} :
a b
@[simp]
theorem Set.Iic.isCoatom_iff {α : Type u_1} [] {b : α} {a : ()} :
a b
theorem covBy_iff_atom_Ici {α : Type u_1} [] {a : α} {b : α} (h : a b) :
a b IsAtom b, h
theorem covBy_iff_coatom_Iic {α : Type u_1} [] {a : α} {b : α} (h : a b) :
a b IsCoatom a, h
theorem IsAtom.inf_eq_bot_of_ne {α : Type u_1} [] [] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
a b =
theorem IsAtom.disjoint_of_ne {α : Type u_1} [] [] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
theorem IsCoatom.sup_eq_top_of_ne {α : Type u_1} [] [] {a : α} {b : α} (ha : ) (hb : ) (hab : a b) :
a b =
theorem isAtomic_iff (α : Type u_1) [] [] :
∀ (b : α), b = ∃ (a : α), a b
class IsAtomic (α : Type u_1) [] [] :

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

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

Every element other than ⊥ has an atom below it.

Instances
theorem IsAtomic.eq_bot_or_exists_atom_le {α : Type u_1} [] [] [self : ] (b : α) :
b = ∃ (a : α), a b

Every element other than ⊥ has an atom below it.

theorem isCoatomic_iff (α : Type u_1) [] [] :
∀ (b : α), b = ∃ (a : α), b a
class IsCoatomic (α : Type u_1) [] [] :

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

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

Every element other than ⊤ has an atom above it.

Instances
theorem IsCoatomic.eq_top_or_exists_le_coatom {α : Type u_1} [] [] [self : ] (b : α) :
b = ∃ (a : α), b a

Every element other than ⊤ has an atom above it.

@[simp]
theorem isCoatomic_dual_iff_isAtomic {α : Type u_1} [] [] :
@[simp]
theorem isAtomic_dual_iff_isCoatomic {α : Type u_1} [] [] :
instance IsAtomic.isCoatomic_dual {α : Type u_1} [] [] [] :
Equations
• =
instance IsAtomic.Set.Iic.isAtomic {α : Type u_1} [] [] [] {x : α} :
IsAtomic ()
Equations
• =
instance IsCoatomic.isCoatomic {α : Type u_1} [] [] [] :
Equations
• =
instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_1} [] [] [] {x : α} :
Equations
• =
theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_1} [] [] :
∀ (x : α), IsAtomic ()
theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_1} [] [] :
∀ (x : α), IsCoatomic ()
theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [] [] (h : WellFounded fun (x x_1 : α) => x < x_1) :
theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [] [] (h : WellFounded fun (x x_1 : α) => x > x_1) :
theorem BooleanAlgebra.le_iff_atom_le_imp {α : Type u_3} [] [] {x : α} {y : α} :
x y ∀ (a : α), a xa y
theorem BooleanAlgebra.eq_iff_atom_le_iff {α : Type u_3} [] [] {x : α} {y : α} :
x = y ∀ (a : α), (a x a y)
@[reducible, inline]
Equations
• CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra = let __spread.0 := inst✝;
Instances For
class IsAtomistic (α : Type u_1) [] :

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

• eq_sSup_atoms : ∀ (b : α), ∃ (s : Set α), b = sSup s as,

Every element is a sSup of a set of atoms.

Instances
theorem IsAtomistic.eq_sSup_atoms {α : Type u_1} [] [self : ] (b : α) :
∃ (s : Set α), b = sSup s as,

Every element is a sSup of a set of atoms.

class IsCoatomistic (α : Type u_1) [] :

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

• eq_sInf_coatoms : ∀ (b : α), ∃ (s : Set α), b = sInf s as,

Every element is a sInf of a set of coatoms.

Instances
theorem IsCoatomistic.eq_sInf_coatoms {α : Type u_1} [] [self : ] (b : α) :
∃ (s : Set α), b = sInf s as,

Every element is a sInf of a set of coatoms.

@[simp]
@[simp]
instance IsAtomistic.isCoatomistic_dual {α : Type u_1} [] [h : ] :
Equations
• =
@[instance 100]
instance IsAtomistic.instIsAtomic {α : Type u_1} [] [] :
Equations
• =
@[simp]
theorem sSup_atoms_le_eq {α : Type u_1} [] [] (b : α) :
sSup {a : α | a b} = b
@[simp]
theorem sSup_atoms_eq_top {α : Type u_1} [] [] :
sSup {a : α | } =
theorem le_iff_atom_le_imp {α : Type u_1} [] [] {a : α} {b : α} :
a b ∀ (c : α), c ac b
theorem eq_iff_atom_le_iff {α : Type u_1} [] [] {a : α} {b : α} :
a = b ∀ (c : α), (c a c b)
instance IsCoatomistic.isAtomistic_dual {α : Type u_1} [] [h : ] :
Equations
• =
@[instance 100]
instance IsCoatomistic.instIsCoatomic {α : Type u_1} [] [] :
Equations
• =
Equations
• =
Equations
• =
class IsSimpleOrder (α : Type u_3) [LE α] [] extends :

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

• exists_pair_ne : ∃ (x : α) (y : α), x y
• eq_bot_or_eq_top : ∀ (a : α), a = a =

Every element is either ⊥ or ⊤

Instances
theorem IsSimpleOrder.eq_bot_or_eq_top {α : Type u_3} [LE α] [] [self : ] (a : α) :
a = a =

Every element is either ⊥ or ⊤

theorem IsSimpleOrder.bot_ne_top {α : Type u_1} [LE α] [] [] :
instance instIsSimpleOrderOrderDual {α : Type u_3} [LE α] [] [] :
Equations
• =
def IsSimpleOrder.preorder {α : Type u_3} [LE α] [] [] :

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

Equations
Instances For
def IsSimpleOrder.linearOrder {α : Type u_1} [] [] [] [] :

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.
Instances For
@[simp]
theorem isAtom_top {α : Type u_1} [] [] [] :
@[simp]
theorem isCoatom_bot {α : Type u_1} [] [] [] :
theorem bot_covBy_top {α : Type u_1} [] [] [] :
theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_1} [] [] [] {a : α} {b : α} (h : a < b) :
a =
theorem IsSimpleOrder.eq_top_of_lt {α : Type u_1} [] [] [] {a : α} {b : α} (h : a < b) :
b =
theorem IsSimpleOrder.LT.lt.eq_bot {α : Type u_1} [] [] [] {a : α} {b : α} (h : a < b) :
a =

Alias of IsSimpleOrder.eq_bot_of_lt.

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

Alias of IsSimpleOrder.eq_top_of_lt.

def IsSimpleOrder.lattice {α : Type u_3} [] [] [] [] :

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

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

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

Equations
• IsSimpleOrder.distribLattice = let __src := inferInstance;
Instances For
@[instance 100]
instance IsSimpleOrder.instIsAtomic {α : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance IsSimpleOrder.instIsCoatomic {α : Type u_1} [] [] [] :
Equations
• =
@[simp]
theorem IsSimpleOrder.equivBool_apply {α : Type u_3} [] [LE α] [] [] (x : α) :
IsSimpleOrder.equivBool x = decide (x = )
@[simp]
theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_3} [] [LE α] [] [] (x : Bool) :
IsSimpleOrder.equivBool.symm x =
def IsSimpleOrder.equivBool {α : Type u_3} [] [LE α] [] [] :

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

Equations
• IsSimpleOrder.equivBool = { toFun := fun (x : α) => decide (x = ), invFun := fun (x : Bool) => , left_inv := , right_inv := }
Instances For
def IsSimpleOrder.orderIsoBool {α : Type u_1} [] [] [] [] :

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

Equations
• IsSimpleOrder.orderIsoBool = let __src := IsSimpleOrder.equivBool; { toEquiv := __src, map_rel_iff' := }
Instances For
def IsSimpleOrder.booleanAlgebra {α : Type u_3} [] [] [] [] :

A simple BoundedOrder is also a BooleanAlgebra.

Equations
• IsSimpleOrder.booleanAlgebra = let __src := ; let __src_1 := IsSimpleOrder.distribLattice; BooleanAlgebra.mk
Instances For
noncomputable def IsSimpleOrder.completeLattice {α : Type u_1} [] [] [] :

A simple BoundedOrder is also complete.

Equations
• IsSimpleOrder.completeLattice = let __src := inferInstance; let __src_1 := inferInstance; CompleteLattice.mk
Instances For
noncomputable def IsSimpleOrder.completeBooleanAlgebra {α : Type u_1} [] [] [] :

A simple BoundedOrder is also a CompleteBooleanAlgebra.

Equations
Instances For
instance IsSimpleOrder.instComplementedLattice {α : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance IsSimpleOrder.instIsAtomistic {α : Type u_1} [] [] :
Equations
• =
instance IsSimpleOrder.instIsCoatomistic {α : Type u_1} [] [] :
Equations
• =
theorem isSimpleOrder_iff_isAtom_top {α : Type u_1} [] [] :
theorem isSimpleOrder_iff_isCoatom_bot {α : Type u_1} [] [] :
theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_1} [] [] {a : α} :
theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_1} [] [] {a : α} :
theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [] [] [] [] (f : β ↪o α) (hbot : f = ) {b : β} (hb : IsAtom (f b)) :
theorem OrderEmbedding.isCoatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [] [] [] [] (f : β ↪o α) (htop : f = ) {b : β} (hb : IsCoatom (f b)) :
theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_1} {β : Type u_2} [] [] [] [] {l : αβ} {u : βα} (gi : ) (hbot : u = ) {b : β} (hb : IsAtom (u b)) :
theorem GaloisInsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [] [] [] [] [] {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} [] [] [] [] [] {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} [] [] [] [] {l : αβ} {u : βα} (gi : ) {b : β} (hb : IsCoatom (u b)) :
theorem GaloisInsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [] [] [] [] [] {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} [] [] [] [] {l : αβ} {u : βα} (gi : ) (hbot : l = ) {a : α} (hb : IsCoatom (l a)) :
theorem GaloisCoinsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [] [] [] [] [] {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} [] [] [] [] [] {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} [] [] [] [] {l : αβ} {u : βα} (gi : ) {a : α} (hb : IsAtom (l a)) :
theorem GaloisCoinsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [] [] [] [] [] {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} [] [] [] [] (f : α ≃o β) (a : α) :
IsAtom (f a)
@[simp]
theorem OrderIso.isCoatom_iff {α : Type u_1} {β : Type u_2} [] [] [] [] (f : α ≃o β) (a : α) :
IsCoatom (f a)
theorem OrderIso.isSimpleOrder_iff {α : Type u_1} {β : Type u_2} [] [] [] [] (f : α ≃o β) :
theorem OrderIso.isSimpleOrder {α : Type u_1} {β : Type u_2} [] [] [] [] [h : ] (f : α ≃o β) :
theorem OrderIso.isAtomic_iff {α : Type u_1} {β : Type u_2} [] [] [] [] (f : α ≃o β) :
theorem OrderIso.isCoatomic_iff {α : Type u_1} {β : Type u_2} [] [] [] [] (f : α ≃o β) :
theorem IsCompl.isAtom_iff_isCoatom {α : Type u_1} [] [] [] {a : α} {b : α} (hc : IsCompl a b) :
theorem IsCompl.isCoatom_iff_isAtom {α : Type u_1} [] [] [] {a : α} {b : α} (hc : IsCompl a b) :
theorem isAtomic_iff_isCoatomic {α : Type u_1} [] [] [] :
@[simp]
theorem Prop.isAtom_iff {p : Prop} :
p
@[simp]
theorem Prop.isCoatom_iff {p : Prop} :
Equations
theorem Pi.eq_bot_iff {ι : Type u_3} {π : ιType u} [(i : ι) → Bot (π i)] {f : (i : ι) → π i} :
f = ∀ (i : ι), f i =
theorem Pi.isAtom_iff {ι : Type u_3} {π : ιType u} {f : (i : ι) → π i} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] :
∃ (i : ι), IsAtom (f i) ∀ (j : ι), j if j =
theorem Pi.isAtom_single {ι : Type u_3} {π : ιType u} {i : ι} [] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {a : π i} (h : ) :
theorem Pi.isAtom_iff_eq_single {ι : Type u_3} {π : ιType u} [] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {f : (i : ι) → π i} :
∃ (i : ι) (a : π i), f =
instance Pi.isAtomic {ι : Type u_3} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomic (π i)] :
IsAtomic ((i : ι) → π i)
Equations
• =
instance Pi.isCoatomic {ι : Type u_3} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
IsCoatomic ((i : ι) → π i)
Equations
• =
instance Pi.isAtomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsAtomistic (π i)] :
IsAtomistic ((i : ι) → π i)
Equations
• =
instance Pi.isCoatomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
IsCoatomistic ((i : ι) → π i)
Equations
• =
@[simp]
theorem isAtom_compl {α : Type u_1} [] {a : α} :
@[simp]
theorem isCoatom_compl {α : Type u_1} [] {a : α} :
theorem IsAtom.of_compl {α : Type u_1} [] {a : α} :

Alias of the forward direction of isAtom_compl.

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

Alias of the reverse direction of isAtom_compl.

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

Alias of the reverse direction of isCoatom_compl.

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

Alias of the forward direction of isCoatom_compl.

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 : α) :
instance Set.instIsAtomistic {α : Type u_1} :
Equations
• =
instance Set.instIsCoatomistic {α : Type u_1} :
Equations
• =