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.
• IsStronglyAtomic indicates that for all a < b, there is some x with a ⋖ x ≤ b.
• IsStronglyCoatomic indicates that for all a < b, there is some x with a ≤ x ⋖ b.

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_2} [Preorder α] [OrderBot α] (a : α) : Prop

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

Equations

• IsAtom a = (a ≠ ⊥ ∧ ∀ b < a, b = ⊥)

theorem IsAtom.Iic {α : Type u_2} [Preorder α] [OrderBot α] {a x : α} (ha : IsAtom a) (hax : a ≤ x) : IsAtom ⟨a, hax⟩

theorem IsAtom.of_isAtom_coe_Iic {α : Type u_2} [Preorder α] [OrderBot α] {x : α} {a : ↑(Set.Iic x)} (ha : IsAtom a) : IsAtom ↑a

theorem isAtom_iff_le_of_ge {α : Type u_2} [Preorder α] [OrderBot α] {a : α} : IsAtom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b

theorem IsAtom.lt_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a x : α} (h : IsAtom a) : x < a ↔ x = ⊥

theorem IsAtom.le_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a x : α} (h : IsAtom a) : x ≤ a ↔ x = ⊥ ∨ x = a

theorem IsAtom.bot_lt {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} (h : IsAtom a) : ⊥ < a

theorem IsAtom.le_iff_eq {α : Type u_2} [PartialOrder α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : b ≠ ⊥) : b ≤ a ↔ b = a

theorem IsAtom.Iic_eq {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} (h : IsAtom a) : Set.Iic a = {⊥, a}

@[simp]

theorem bot_covBy_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} : ⊥ ⋖ a ↔ IsAtom a

theorem CovBy.is_atom {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} : ⊥ ⋖ a → IsAtom a

Alias of the forward direction of bot_covBy_iff.

theorem IsAtom.bot_covBy {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} : IsAtom a → ⊥ ⋖ a

Alias of the reverse direction of bot_covBy_iff.

theorem atom_le_iSup {ι : Sort u_1} {α : Type u_2} [Order.Frame α] {a : α} (ha : IsAtom a) {f : ι → α} : a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i

def IsCoatom {α : Type u_2} [Preorder α] [OrderTop α] (a : α) : Prop

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

Equations

• IsCoatom a = (a ≠ ⊤ ∧ ∀ (b : α), a < b → b = ⊤)

@[simp]

theorem isCoatom_dual_iff_isAtom {α : Type u_2} [Preorder α] [OrderBot α] {a : α} : IsCoatom (OrderDual.toDual a) ↔ IsAtom a

@[simp]

theorem isAtom_dual_iff_isCoatom {α : Type u_2} [Preorder α] [OrderTop α] {a : α} : IsAtom (OrderDual.toDual a) ↔ IsCoatom a

theorem IsAtom.dual {α : Type u_2} [Preorder α] [OrderBot α] {a : α} : IsAtom a → IsCoatom (OrderDual.toDual a)

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

theorem IsCoatom.dual {α : Type u_2} [Preorder α] [OrderTop α] {a : α} : IsCoatom a → IsAtom (OrderDual.toDual a)

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

theorem IsCoatom.Ici {α : Type u_2} [Preorder α] [OrderTop α] {a x : α} (ha : IsCoatom a) (hax : x ≤ a) : IsCoatom ⟨a, hax⟩

theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_2} [Preorder α] [OrderTop α] {x : α} {a : ↑(Set.Ici x)} (ha : IsCoatom a) : IsCoatom ↑a

theorem isCoatom_iff_ge_of_le {α : Type u_2} [Preorder α] [OrderTop α] {a : α} : IsCoatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a

theorem IsCoatom.lt_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a x : α} (h : IsCoatom a) : a < x ↔ x = ⊤

theorem IsCoatom.le_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a x : α} (h : IsCoatom a) : a ≤ x ↔ x = ⊤ ∨ x = a

theorem IsCoatom.lt_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} (h : IsCoatom a) : a < ⊤

theorem IsCoatom.le_iff_eq {α : Type u_2} [PartialOrder α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : b ≠ ⊤) : a ≤ b ↔ b = a

theorem IsCoatom.Ici_eq {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} (h : IsCoatom a) : Set.Ici a = {⊤, a}

@[simp]

theorem covBy_top_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} : a ⋖ ⊤ ↔ IsCoatom a

theorem IsCoatom.covBy_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} : IsCoatom a → a ⋖ ⊤

Alias of the reverse direction of covBy_top_iff.

theorem CovBy.isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} : a ⋖ ⊤ → IsCoatom a

Alias of the forward direction of covBy_top_iff.

theorem SetLike.isAtom_iff {A : Type u_4} {B : Type u_5} [SetLike A B] [OrderBot A] {K : A} : IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

theorem SetLike.isCoatom_iff {A : Type u_4} {B : Type u_5} [SetLike A B] [OrderTop A] {K : A} : IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

theorem SetLike.covBy_iff {A : Type u_4} {B : Type u_5} [SetLike A B] {K L : A} : K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

theorem SetLike.covBy_iff' {A : Type u_4} {B : Type u_5} [SetLike A B] {K L : A} : K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Dual variant of SetLike.covBy_iff

theorem iInf_le_coatom {ι : Sort u_1} {α : Type u_2} [Order.Coframe α] {a : α} (ha : IsCoatom a) {f : ι → α} : iInf f ≤ a ↔ ∃ (i : ι), f i ≤ a

@[simp]

theorem Set.Ici.isAtom_iff {α : Type u_2} [PartialOrder α] {a : α} {b : ↑(Ici a)} : IsAtom b ↔ a ⋖ ↑b

@[simp]

theorem Set.Iic.isCoatom_iff {α : Type u_2} [PartialOrder α] {b : α} {a : ↑(Iic b)} : IsCoatom a ↔ ↑a ⋖ b

theorem covBy_iff_atom_Ici {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) : a ⋖ b ↔ IsAtom ⟨b, h⟩

theorem covBy_iff_coatom_Iic {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) : a ⋖ b ↔ IsCoatom ⟨a, h⟩

theorem IsAtom.inf_eq_bot_of_ne {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : a ⊓ b = ⊥

theorem IsAtom.disjoint_of_ne {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : Disjoint a b

theorem IsCoatom.sup_eq_top_of_ne {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : a ⊔ b = ⊤

theorem IsCoatom.codisjoint_of_ne {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : Codisjoint a b

class IsAtomic (α : Type u_2) [PartialOrder α] [OrderBot α] : Prop

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

• eq_bot_or_exists_atom_le (b : α) : b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

  Every element other than ⊥ has an atom below it.

theorem isAtomic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] : IsAtomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

class IsCoatomic (α : Type u_2) [PartialOrder α] [OrderTop α] : Prop

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

• eq_top_or_exists_le_coatom (b : α) : b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

  Every element other than ⊤ has an atom above it.

theorem isCoatomic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] : IsCoatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

theorem IsAtomic.exists_atom (α : Type u_2) [PartialOrder α] [OrderBot α] [Nontrivial α] [IsAtomic α] : ∃ (a : α), IsAtom a

theorem IsCoatomic.exists_coatom (α : Type u_2) [PartialOrder α] [OrderTop α] [Nontrivial α] [IsCoatomic α] : ∃ (a : α), IsCoatom a

@[simp]

theorem isCoatomic_dual_iff_isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] : IsCoatomic αᵒᵈ ↔ IsAtomic α

@[simp]

theorem isAtomic_dual_iff_isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] : IsAtomic αᵒᵈ ↔ IsCoatomic α

instance OrderDual.instIsCoatomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] : IsCoatomic αᵒᵈ

instance IsAtomic.Set.Iic.isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] {x : α} : IsAtomic ↑(Set.Iic x)

instance OrderDual.instIsAtomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] : IsAtomic αᵒᵈ

instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] {x : α} : IsCoatomic ↑(Set.Ici x)

theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_2} [PartialOrder α] [OrderBot α] : IsAtomic α ↔ ∀ (x : α), IsAtomic ↑(Set.Iic x)

theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_2} [PartialOrder α] [OrderTop α] : IsCoatomic α ↔ ∀ (x : α), IsCoatomic ↑(Set.Ici x)

class IsStronglyAtomic (α : Type u_5) [Preorder α] : Prop

An order is strongly atomic if every nontrivial interval [a, b] contains an element covering a.

• exists_covBy_le_of_lt (a b : α) : a < b → ∃ (x : α), a ⋖ x ∧ x ≤ b

theorem isStronglyAtomic_iff (α : Type u_5) [Preorder α] : IsStronglyAtomic α ↔ ∀ (a b : α), a < b → ∃ (x : α), a ⋖ x ∧ x ≤ b

theorem exists_covBy_le_of_lt {α : Type u_4} {a b : α} [Preorder α] [IsStronglyAtomic α] (h : a < b) : ∃ (x : α), a ⋖ x ∧ x ≤ b

theorem LT.lt.exists_covby_le {α : Type u_4} {a b : α} [Preorder α] [IsStronglyAtomic α] (h : a < b) : ∃ (x : α), a ⋖ x ∧ x ≤ b

Alias of exists_covBy_le_of_lt.

class IsStronglyCoatomic (α : Type u_5) [Preorder α] : Prop

An order is strongly coatomic if every nontrivial interval [a, b] contains an element covered by b.

• exists_le_covBy_of_lt (a b : α) : a < b → ∃ (x : α), a ≤ x ∧ x ⋖ b

theorem isStronglyCoatomic_iff (α : Type u_5) [Preorder α] : IsStronglyCoatomic α ↔ ∀ (a b : α), a < b → ∃ (x : α), a ≤ x ∧ x ⋖ b

theorem exists_le_covBy_of_lt {α : Type u_4} {a b : α} [Preorder α] [IsStronglyCoatomic α] (h : a < b) : ∃ (x : α), a ≤ x ∧ x ⋖ b

theorem LT.lt.exists_le_covby {α : Type u_4} {a b : α} [Preorder α] [IsStronglyCoatomic α] (h : a < b) : ∃ (x : α), a ≤ x ∧ x ⋖ b

Alias of exists_le_covBy_of_lt.

theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic {α : Type u_4} [Preorder α] : IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

@[simp]

theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic {α : Type u_4} [Preorder α] : IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

instance OrderDual.instIsStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyAtomic α] : IsStronglyCoatomic αᵒᵈ

instance instIsStronglyAtomicOrderDualOfIsStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ

instance IsStronglyAtomic.isAtomic (α : Type u_5) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] : IsAtomic α

instance IsStronglyCoatomic.toIsCoatomic (α : Type u_5) [PartialOrder α] [OrderTop α] [IsStronglyCoatomic α] : IsCoatomic α

theorem Set.OrdConnected.isStronglyAtomic {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} (h : s.OrdConnected) : IsStronglyAtomic ↑s

theorem Set.OrdConnected.isStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} (h : s.OrdConnected) : IsStronglyCoatomic ↑s

instance instIsStronglyAtomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} [s.OrdConnected] : IsStronglyAtomic ↑s

instance instIsStronglyCoatomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} [h : s.OrdConnected] : IsStronglyCoatomic ↑s

instance SuccOrder.toIsStronglyAtomic {α : Type u_4} [Preorder α] [SuccOrder α] : IsStronglyAtomic α

instance instIsStronglyCoatomicOfPredOrder {α : Type u_4} [Preorder α] [PredOrder α] : IsStronglyCoatomic α

theorem IsStronglyAtomic.of_wellFounded_lt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) : IsStronglyAtomic α

theorem IsStronglyCoatomic.of_wellFounded_gt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) : IsStronglyCoatomic α

instance instIsStronglyAtomicOfWellFoundedLT {α : Type u_2} [PartialOrder α] [WellFoundedLT α] : IsStronglyAtomic α

instance instIsStronglyCoatomicOfWellFoundedGT {α : Type u_2} [PartialOrder α] [WellFoundedGT α] : IsStronglyCoatomic α

theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_2} [PartialOrder α] [OrderBot α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) : IsAtomic α

theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_2} [PartialOrder α] [OrderTop α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) : IsCoatomic α

theorem BooleanAlgebra.le_iff_atom_le_imp {α : Type u_4} [BooleanAlgebra α] [IsAtomic α] {x y : α} : x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y

theorem BooleanAlgebra.eq_iff_atom_le_iff {α : Type u_4} [BooleanAlgebra α] [IsAtomic α] {x y : α} : x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

@[reducible, inline]

abbrev CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra {α : Type u_4} [CompleteBooleanAlgebra α] [IsAtomic α] : CompleteAtomicBooleanAlgebra α

Equations

• CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

class IsAtomistic (α : Type u_2) [PartialOrder α] [OrderBot α] : Prop

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

• isLUB_atoms (b : α) : ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a

  Every element is a sSup of a set of atoms.

theorem isAtomistic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] : IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a

class IsCoatomistic (α : Type u_2) [PartialOrder α] [OrderTop α] : Prop

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

• isGLB_coatoms (b : α) : ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

  Every element is a sInf of a set of coatoms.

theorem isCoatomistic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] : IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

@[simp]

theorem isCoatomistic_dual_iff_isAtomistic {α : Type u_2} [PartialOrder α] [OrderBot α] : IsCoatomistic αᵒᵈ ↔ IsAtomistic α

@[simp]

theorem isAtomistic_dual_iff_isCoatomistic {α : Type u_2} [PartialOrder α] [OrderTop α] : IsAtomistic αᵒᵈ ↔ IsCoatomistic α

instance OrderDual.instIsCoatomistic {α : Type u_2} [PartialOrder α] [OrderBot α] [h : IsAtomistic α] : IsCoatomistic αᵒᵈ

@[instance 100]

instance IsAtomistic.instIsAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] : IsAtomic α

theorem isLUB_atoms_le {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] (b : α) : IsLUB {a : α | IsAtom a ∧ a ≤ b} b

theorem isLUB_atoms_top {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] [OrderTop α] : IsLUB {a : α | IsAtom a} ⊤

theorem le_iff_atom_le_imp {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} : a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b

theorem eq_iff_atom_le_iff {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} : a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

instance OrderDual.instIsAtomistic {α : Type u_2} [PartialOrder α] [OrderTop α] [h : IsCoatomistic α] : IsAtomistic αᵒᵈ

@[instance 100]

instance IsCoatomistic.instIsCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomistic α] : IsCoatomic α

@[simp]

theorem sSup_atoms_le_eq {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) : sSup {a : α | IsAtom a ∧ a ≤ b} = b

@[simp]

theorem sSup_atoms_eq_top {α : Type u_4} [CompleteLattice α] [IsAtomistic α] : sSup {a : α | IsAtom a} = ⊤

theorem CompleteLattice.isAtomistic_iff {α : Type u_4} [CompleteLattice α] : IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

theorem eq_sSup_atoms {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) : ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

theorem CompleteLattice.isCoatomistic_iff {α : Type u_4} [CompleteLattice α] : IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a

theorem eq_sInf_coatoms {α : Type u_4} [CompleteLattice α] [IsCoatomistic α] (b : α) : ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a

instance CompleteAtomicBooleanAlgebra.instIsAtomistic {α : Type u_4} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α

instance CompleteAtomicBooleanAlgebra.instIsCoatomistic {α : Type u_4} [CompleteAtomicBooleanAlgebra α] : IsCoatomistic α

class IsSimpleOrder (α : Type u_4) [LE α] [BoundedOrder α] extends Nontrivial α : Prop

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 ⊤

theorem isSimpleOrder_iff_isSimpleOrder_orderDual {α : Type u_2} [LE α] [BoundedOrder α] : IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

theorem IsSimpleOrder.bot_ne_top {α : Type u_2} [LE α] [BoundedOrder α] [IsSimpleOrder α] : ⊥ ≠ ⊤

instance OrderDual.instIsSimpleOrder {α : Type u_4} [LE α] [BoundedOrder α] [IsSimpleOrder α] : IsSimpleOrder αᵒᵈ

def IsSimpleOrder.preorder {α : Type u_4} [LE α] [BoundedOrder α] [IsSimpleOrder α] : Preorder α

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

Equations

• IsSimpleOrder.preorder = Preorder.mk ⋯ ⋯ ⋯

def IsSimpleOrder.linearOrder {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] : LinearOrder α

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_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : IsAtom ⊤

@[simp]

theorem isCoatom_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : IsCoatom ⊥

theorem bot_covBy_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : ⊥ ⋖ ⊤

theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) : a = ⊥

theorem IsSimpleOrder.eq_top_of_lt {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) : b = ⊤

theorem LT.lt.eq_bot {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) : a = ⊥

Alias of IsSimpleOrder.eq_bot_of_lt.

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

Alias of IsSimpleOrder.eq_top_of_lt.

def IsSimpleOrder.lattice {α : Type u_4} [DecidableEq α] [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : Lattice α

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_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : DistribLattice α

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

Equations

• IsSimpleOrder.distribLattice = DistribLattice.mk ⋯

@[instance 100]

instance IsSimpleOrder.instIsAtomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : IsAtomic α

@[instance 100]

instance IsSimpleOrder.instIsCoatomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : IsCoatomic α

def IsSimpleOrder.equivBool {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : α ≃ Bool

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

Equations

• IsSimpleOrder.equivBool = { toFun := fun (x : α) => decide (x = ⊤), invFun := fun (x : Bool) => Bool.casesOn x ⊥ ⊤, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem IsSimpleOrder.equivBool_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : α) : equivBool x = decide (x = ⊤)

@[simp]

theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : Bool) : equivBool.symm x = Bool.casesOn x ⊥ ⊤

def IsSimpleOrder.orderIsoBool {α : Type u_2} [DecidableEq α] [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : α ≃o Bool

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

Equations

• IsSimpleOrder.orderIsoBool = { toEquiv := IsSimpleOrder.equivBool, map_rel_iff' := ⋯ }

def IsSimpleOrder.booleanAlgebra {α : Type u_4} [DecidableEq α] [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : BooleanAlgebra α

A simple BoundedOrder is also a BooleanAlgebra.

Equations

• IsSimpleOrder.booleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def IsSimpleOrder.completeLattice {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : CompleteLattice α

A simple BoundedOrder is also complete.

Equations

• IsSimpleOrder.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def IsSimpleOrder.completeBooleanAlgebra {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : CompleteBooleanAlgebra α

A simple BoundedOrder is also a CompleteBooleanAlgebra.

Equations

• IsSimpleOrder.completeBooleanAlgebra = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance IsSimpleOrder.instComplementedLattice {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : ComplementedLattice α

@[instance 100]

instance IsSimpleOrder.instIsAtomistic {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : IsAtomistic α

@[instance 100]

instance IsSimpleOrder.instIsCoatomistic {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : IsCoatomistic α

theorem isSimpleOrder_iff_isAtom_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsAtom ⊤

theorem isSimpleOrder_iff_isCoatom_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsCoatom ⊥

theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} : IsSimpleOrder ↑(Iic a) ↔ IsAtom a

theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} : IsSimpleOrder ↑(Ici a) ↔ IsCoatom a

theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β} (hb : IsAtom (f b)) : IsAtom b

theorem OrderEmbedding.isCoatom_of_map_top_of_image {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : β ↪o α) (htop : f ⊤ = ⊤) {b : β} (hb : IsCoatom (f b)) : IsCoatom b

theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) {b : β} (hb : IsAtom (u b)) : IsAtom b

theorem GaloisInsertion.isAtom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), IsAtom a → u (l a) = a) (a : α) : IsAtom (l a) ↔ IsAtom a

theorem GaloisInsertion.isAtom_iff' {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), IsAtom a → u (l a) = a) (b : β) : IsAtom (u b) ↔ IsAtom b

theorem GaloisInsertion.isCoatom_of_image {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) : IsCoatom b

theorem GaloisInsertion.isCoatom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [IsCoatomic α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a) (b : β) : IsCoatom (u b) ↔ IsCoatom b

theorem GaloisCoinsertion.isCoatom_of_l_top {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (hbot : l ⊤ = ⊤) {a : α} (hb : IsCoatom (l a)) : IsCoatom a

theorem GaloisCoinsertion.isCoatom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b) (b : β) : IsCoatom (u b) ↔ IsCoatom b

theorem GaloisCoinsertion.isCoatom_iff' {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b) (a : α) : IsCoatom (l a) ↔ IsCoatom a

theorem GaloisCoinsertion.isAtom_of_image {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) : IsAtom a

theorem GaloisCoinsertion.isAtom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] [IsAtomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (h_atom : ∀ (b : β), IsAtom b → l (u b) = b) (a : α) : IsAtom (l a) ↔ IsAtom a

@[simp]

theorem OrderIso.isAtom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) : IsAtom (f a) ↔ IsAtom a

@[simp]

theorem OrderIso.isCoatom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) (a : α) : IsCoatom (f a) ↔ IsCoatom a

theorem OrderIso.isSimpleOrder_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) : IsSimpleOrder α ↔ IsSimpleOrder β

theorem OrderIso.isSimpleOrder {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) : IsSimpleOrder α

theorem OrderIso.isAtomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) : IsAtomic α ↔ IsAtomic β

theorem OrderIso.isCoatomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) : IsCoatomic α ↔ IsCoatomic β

theorem Lattice.isStronglyAtomic {α : Type u_2} [Lattice α] [OrderBot α] [IsUpperModularLattice α] [IsAtomistic α] : IsStronglyAtomic α

An upper-modular lattice that is atomistic is strongly atomic. Not an instance to prevent loops.

@[deprecated Lattice.isStronglyAtomic (since := "2025-03-13")]

theorem CompleteLattice.isStronglyAtomic {α : Type u_2} [Lattice α] [OrderBot α] [IsUpperModularLattice α] [IsAtomistic α] : IsStronglyAtomic α

Alias of Lattice.isStronglyAtomic.

---

An upper-modular lattice that is atomistic is strongly atomic. Not an instance to prevent loops.

theorem Lattice.isStronglyCoatomic {α : Type u_2} [Lattice α] [OrderTop α] [IsLowerModularLattice α] [IsCoatomistic α] : IsStronglyCoatomic α

A lower-modular lattice that is coatomistic is strongly coatomic. Not an instance to prevent loops.

@[deprecated Lattice.isStronglyCoatomic (since := "2025-03-13")]

theorem CompleteLattice.isStronglyCoatomic {α : Type u_2} [Lattice α] [OrderTop α] [IsLowerModularLattice α] [IsCoatomistic α] : IsStronglyCoatomic α

Alias of Lattice.isStronglyCoatomic.

---

A lower-modular lattice that is coatomistic is strongly coatomic. Not an instance to prevent loops.

theorem IsCompl.isAtom_iff_isCoatom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (hc : IsCompl a b) : IsAtom a ↔ IsCoatom b

theorem IsCompl.isCoatom_iff_isAtom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (hc : IsCompl a b) : IsCoatom a ↔ IsAtom b

theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsAtomic α] : IsCoatomic α

theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsCoatomic α] : IsAtomic α

theorem isAtomic_iff_isCoatomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] : IsAtomic α ↔ IsCoatomic α

theorem ComplementedLattice.isStronglyAtomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsAtomic α] : IsStronglyAtomic α

A complemented modular atomic lattice is strongly atomic. Not an instance to prevent loops.

theorem ComplementedLattice.isStronglyCoatomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsCoatomic α] : IsStronglyCoatomic α

A complemented modular coatomic lattice is strongly coatomic. Not an instance to prevent loops.

theorem ComplementedLattice.isStronglyAtomic' {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [h : IsAtomic α] : IsStronglyCoatomic α

A complemented modular atomic lattice is strongly coatomic. Not an instance to prevent loops.

theorem ComplementedLattice.isStronglyCoatomic' {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [h : IsCoatomic α] : IsStronglyAtomic α

A complemented modular coatomic lattice is strongly atomic. Not an instance to prevent loops.

@[simp]

theorem Prop.isAtom_iff {p : Prop} : IsAtom p ↔ p

@[simp]

theorem Prop.isCoatom_iff {p : Prop} : IsCoatom p ↔ ¬p

instance Prop.instIsSimpleOrderProp : IsSimpleOrder Prop

theorem Pi.eq_bot_iff {ι : Type u_4} {π : ι → Type u} [(i : ι) → Bot (π i)] {f : (i : ι) → π i} : f = ⊥ ↔ ∀ (i : ι), f i = ⊥

theorem Pi.isAtom_iff {ι : Type u_4} {π : ι → Type u} {f : (i : ι) → π i} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] : IsAtom f ↔ ∃ (i : ι), IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

theorem Pi.isAtom_single {ι : Type u_4} {π : ι → Type u} {i : ι} [DecidableEq ι] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {a : π i} (h : IsAtom a) : IsAtom (Function.update ⊥ i a)

theorem Pi.isAtom_iff_eq_single {ι : Type u_4} {π : ι → Type u} [DecidableEq ι] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {f : (i : ι) → π i} : IsAtom f ↔ ∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update ⊥ i a

instance Pi.isAtomic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomic (π i)] : IsAtomic ((i : ι) → π i)

instance Pi.isCoatomic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] : IsCoatomic ((i : ι) → π i)

instance Pi.isAtomistic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomistic (π i)] : IsAtomistic ((i : ι) → π i)

instance Pi.isCoatomistic {ι : Type u_4} {π : ι → Type u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] : IsCoatomistic ((i : ι) → π i)

@[simp]

theorem isAtom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsAtom aᶜ ↔ IsCoatom a

@[simp]

theorem isCoatom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsCoatom aᶜ ↔ IsAtom a

theorem IsCoatom.compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsCoatom a → IsAtom aᶜ

Alias of the reverse direction of isAtom_compl.

theorem IsAtom.of_compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsAtom aᶜ → IsCoatom a

Alias of the forward direction of isAtom_compl.

theorem IsCoatom.of_compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsCoatom aᶜ → IsAtom a

Alias of the forward direction of isCoatom_compl.

theorem IsAtom.compl {α : Type u_2} [BooleanAlgebra α] {a : α} : IsAtom a → IsCoatom aᶜ

Alias of the reverse direction of isCoatom_compl.

theorem Set.isAtom_singleton {α : Type u_2} (x : α) : IsAtom {x}

theorem Set.isAtom_iff {α : Type u_2} {s : Set α} : IsAtom s ↔ ∃ (x : α), s = {x}

theorem Set.isCoatom_iff {α : Type u_2} (s : Set α) : IsCoatom s ↔ ∃ (x : α), s = {x}ᶜ

theorem Set.isCoatom_singleton_compl {α : Type u_2} (x : α) : IsCoatom {x}ᶜ

instance Set.instIsAtomistic {α : Type u_2} : IsAtomistic (Set α)

instance Set.instIsCoatomistic {α : Type u_2} : IsCoatomistic (Set α)