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

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

theorem IsAtom.Iic {α : Type u_1} [Preorder α] [OrderBot α] {a : α} {x : α} (ha : IsAtom a) (hax : a ≤ x) : IsAtom { val := a, property := hax }

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

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

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

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

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

@[simp]

theorem bot_covby_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : ⊥ ⋖ a ↔ IsAtom a

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

Alias of the forward direction of bot_covby_iff.

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

Alias of the reverse direction of bot_covby_iff.

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

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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

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

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

theorem IsCoatom.Ici {α : Type u_1} [Preorder α] [OrderTop α] {a : α} {x : α} (ha : IsCoatom a) (hax : x ≤ a) : IsCoatom { val := a, property := hax }

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

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

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

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

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

@[simp]

theorem covby_top_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : a ⋖ ⊤ ↔ IsCoatom a

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

Alias of the reverse direction of covby_top_iff.

theorem Covby.is_coatom {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : a ⋖ ⊤ → IsCoatom a

Alias of the forward direction of covby_top_iff.

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

@[simp]

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

@[simp]

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

theorem covby_iff_atom_Ici {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) : a ⋖ b ↔ IsAtom { val := b, property := h }

theorem covby_iff_coatom_Iic {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) : a ⋖ b ↔ IsCoatom { val := a, property := h }

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

theorem IsAtom.disjoint_of_ne {α : Type u_1} [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_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : a ⊔ b = ⊤

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

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

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

  Every element other than ⊥ has an atom below it.

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

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

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

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

  Every element other than ⊤ has an atom above it.

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

@[simp]

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

@[simp]

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

instance IsAtomic.isCoatomic_dual {α : Type u_1} [PartialOrder α] [OrderBot α] [IsAtomic α] : IsCoatomic αᵒᵈ

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

instance IsCoatomic.isCoatomic {α : Type u_1} [PartialOrder α] [OrderTop α] [IsCoatomic α] : IsAtomic αᵒᵈ

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

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

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

theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [PartialOrder α] [OrderBot α] (h : WellFounded fun x x_1 => x < x_1) : IsAtomic α

theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [PartialOrder α] [OrderTop α] (h : WellFounded fun x x_1 => x > x_1) : IsCoatomic α

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

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

@[inline, reducible]

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

class IsAtomistic (α : Type u_1) [CompleteLattice α] : Prop

• eq_sSup_atoms : ∀ (b : α), ∃ s, b = sSup s ∧ ∀ (a : α), a ∈ s → IsAtom a

  Every element is a sSup of a set of atoms.

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

class IsCoatomistic (α : Type u_1) [CompleteLattice α] : Prop

• eq_sInf_coatoms : ∀ (b : α), ∃ s, b = sInf s ∧ ∀ (a : α), a ∈ s → IsCoatom a

  Every element is a sInf of a set of coatoms.

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

@[simp]

theorem isCoatomistic_dual_iff_isAtomistic {α : Type u_1} [CompleteLattice α] : IsCoatomistic αᵒᵈ ↔ IsAtomistic α

@[simp]

theorem isAtomistic_dual_iff_isCoatomistic {α : Type u_1} [CompleteLattice α] : IsAtomistic αᵒᵈ ↔ IsCoatomistic α

instance IsAtomistic.isCoatomistic_dual {α : Type u_1} [CompleteLattice α] [h : IsAtomistic α] : IsCoatomistic αᵒᵈ

instance IsAtomistic.instIsAtomicToPartialOrderToCompleteSemilatticeInfToOrderBotToLEToPreorderToBoundedOrder {α : Type u_1} [CompleteLattice α] [IsAtomistic α] : IsAtomic α

@[simp]

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

@[simp]

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

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

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

instance IsCoatomistic.isAtomistic_dual {α : Type u_1} [CompleteLattice α] [h : IsCoatomistic α] : IsAtomistic αᵒᵈ

instance IsCoatomistic.instIsCoatomicToPartialOrderToCompleteSemilatticeInfToOrderTopToLEToPreorderToBoundedOrder {α : Type u_1} [CompleteLattice α] [IsCoatomistic α] : IsCoatomic α

instance CompleteAtomicBooleanAlgebra.instIsAtomisticToCompleteLatticeToCompletelyDistribLattice {α : Type u_3} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α

instance CompleteAtomicBooleanAlgebra.instIsCoatomisticToCompleteLatticeToCompletelyDistribLattice {α : Type u_3} [CompleteAtomicBooleanAlgebra α] : IsCoatomistic α

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

• exists_pair_ne : ∃ x y, x ≠ y
• eq_bot_or_eq_top : ∀ (a : α), a = ⊥ ∨ a = ⊤

  Every element is either ⊥ or ⊤

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

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

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

instance instIsSimpleOrderOrderDualInstLEOrderDualBoundedOrder {α : Type u_3} [LE α] [BoundedOrder α] [IsSimpleOrder α] : IsSimpleOrder αᵒᵈ

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

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

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

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

@[simp]

theorem isAtom_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : IsAtom ⊤

@[simp]

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

theorem bot_covby_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : ⊥ ⋖ ⊤

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

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

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

Alias of IsSimpleOrder.eq_bot_of_lt.

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

Alias of IsSimpleOrder.eq_top_of_lt.

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

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

def IsSimpleOrder.distribLattice {α : Type u_1} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : DistribLattice α

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

instance IsSimpleOrder.instIsAtomicToPartialOrderToSemilatticeInfToOrderBotToLEToPreorder {α : Type u_1} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : IsAtomic α

instance IsSimpleOrder.instIsCoatomicToPartialOrderToSemilatticeInfToOrderTopToLEToPreorder {α : Type u_1} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : IsCoatomic α

@[simp]

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

@[simp]

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

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

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

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

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

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

A simple BoundedOrder is also a BooleanAlgebra.

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

A simple BoundedOrder is also complete.

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

A simple BoundedOrder is also a CompleteBooleanAlgebra.

instance IsSimpleOrder.instIsAtomistic {α : Type u_1} [CompleteLattice α] [IsSimpleOrder α] : IsAtomistic α

instance IsSimpleOrder.instIsCoatomistic {α : Type u_1} [CompleteLattice α] [IsSimpleOrder α] : IsCoatomistic α

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

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

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

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

theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : β ↪o α) (htop : ↑f ⊤ = ⊤) {b : β} (hb : IsCoatom (↑f b)) : IsCoatom b

theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) : IsCoatom b

theorem GaloisInsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) : IsAtom a

theorem GaloisCoinsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) : IsAtom (↑f a) ↔ IsAtom a

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

instance Prop.instIsSimpleOrderPropLeBoundedOrder : IsSimpleOrder Prop

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)] : IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

theorem Pi.isAtom_single {ι : Type u_3} {π : ι → 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_3} {π : ι → Type u} [DecidableEq ι] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {f : (i : ι) → π i} : IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

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

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

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

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

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

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

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

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

instance Set.instIsAtomisticSetToCompleteLatticeToCompletelyDistribLatticeCompleteAtomicBooleanAlgebra {α : Type u_1} : IsAtomistic (Set α)

instance Set.instIsCoatomisticSetToCompleteLatticeToCompletelyDistribLatticeCompleteAtomicBooleanAlgebra {α : Type u_1} : IsCoatomistic (Set α)