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

source
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 = ⊥)

Instances For

source
theorem IsAtom.Iic {α : Type u_2} [Preorder α] [OrderBot α] {a x : α} (ha : IsAtom a) (hax : a ≤ x) :
IsAtom ⟨a, hax⟩
source
theorem IsAtom.of_isAtom_coe_Iic {α : Type u_2} [Preorder α] [OrderBot α] {x : α} {a : ↑(Set.Iic x)} (ha : IsAtom a) :
IsAtom ↑a
source
theorem isAtom_iff_le_of_ge {α : Type u_2} [Preorder α] [OrderBot α] {a : α} :
IsAtom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b
source
theorem IsAtom.ne_bot {α : Type u_2} [Preorder α] [OrderBot α] {a : α} (ha : IsAtom a) :
a ≠ ⊥
source
theorem IsAtom.lt_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a x : α} (h : IsAtom a) :
x < a ↔ x = ⊥
source
theorem IsAtom.le_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a x : α} (h : IsAtom a) :
x ≤ a ↔ x = ⊥ ∨ x = a
source
theorem IsAtom.bot_lt {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} (h : IsAtom a) :
⊥ < a
source
theorem IsAtom.le_iff_eq {α : Type u_2} [PartialOrder α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : b ≠ ⊥) :
b ≤ a ↔ b = a
source
theorem IsAtom.ne_iff_eq_bot {α : Type u_2} [PartialOrder α] [OrderBot α] {a b : α} (ha : IsAtom a) (hba : b ≤ a) :
b ≠ a ↔ b = ⊥
source
theorem IsAtom.ne_bot_iff_eq {α : Type u_2} [PartialOrder α] [OrderBot α] {a b : α} (ha : IsAtom a) (hba : b ≤ a) :
b ≠ ⊥ ↔ b = a
source
theorem IsAtom.Iic_eq {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} (h : IsAtom a) :
Set.Iic a = {⊥, a}
source
@[simp]
theorem bot_covBy_iff {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} :
⊥ ⋖ a ↔ IsAtom a
source
theorem CovBy.is_atom {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} :
⊥ ⋖ a → IsAtom a

Alias of the forward direction of `bot_covBy_iff`.

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

Alias of the reverse direction of `bot_covBy_iff`.

source
theorem IsAtom.le_iSup {ι : Sort u_1} {α : Type u_2} [Order.Frame α] {f : ι → α} {a : α} (ha : IsAtom a) :
a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i
source
@[deprecated IsAtom.le_iSup (since := "2025-07-11")]
theorem atom_le_iSup {ι : Sort u_1} {α : Type u_2} [Order.Frame α] {f : ι → α} {a : α} (ha : IsAtom a) :
a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i

Alias of `IsAtom.le_iSup`.

source
theorem IsAtom.le_sSup {α : Type u_2} [Order.Frame α] {s : Set α} {a : α} (ha : IsAtom a) :
a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b
source
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 = ⊤)

Instances For

source
@[simp]
theorem isCoatom_dual_iff_isAtom {α : Type u_2} [Preorder α] [OrderBot α] {a : α} :
IsCoatom (OrderDual.toDual a) ↔ IsAtom a
source
@[simp]
theorem isAtom_dual_iff_isCoatom {α : Type u_2} [Preorder α] [OrderTop α] {a : α} :
IsAtom (OrderDual.toDual a) ↔ IsCoatom a
source
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`.

source
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`.

source
theorem IsCoatom.Ici {α : Type u_2} [Preorder α] [OrderTop α] {a x : α} (ha : IsCoatom a) (hax : x ≤ a) :
IsCoatom ⟨a, hax⟩
source
theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_2} [Preorder α] [OrderTop α] {x : α} {a : ↑(Set.Ici x)} (ha : IsCoatom a) :
IsCoatom ↑a
source
theorem isCoatom_iff_ge_of_le {α : Type u_2} [Preorder α] [OrderTop α] {a : α} :
IsCoatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a
source
theorem IsCoatom.ne_top {α : Type u_2} [Preorder α] [OrderTop α] {a : α} (ha : IsCoatom a) :
a ≠ ⊤
source
theorem IsCoatom.lt_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a x : α} (h : IsCoatom a) :
a < x ↔ x = ⊤
source
theorem IsCoatom.le_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a x : α} (h : IsCoatom a) :
a ≤ x ↔ x = ⊤ ∨ x = a
source
theorem IsCoatom.lt_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} (h : IsCoatom a) :
a < ⊤
source
theorem IsCoatom.le_iff_eq {α : Type u_2} [PartialOrder α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : b ≠ ⊤) :
a ≤ b ↔ b = a
source
theorem IsCoatom.ne_iff_eq_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hab : a ≤ b) :
b ≠ a ↔ b = ⊤
source
theorem IsCoatom.ne_top_iff_eq {α : Type u_2} [PartialOrder α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hab : a ≤ b) :
b ≠ ⊤ ↔ b = a
source
theorem IsCoatom.Ici_eq {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} (h : IsCoatom a) :
Set.Ici a = {⊤, a}
source
@[simp]
theorem covBy_top_iff {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
a ⋖ ⊤ ↔ IsCoatom a
source
theorem CovBy.isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
a ⋖ ⊤ → IsCoatom a

Alias of the forward direction of `covBy_top_iff`.

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

Alias of the reverse direction of `covBy_top_iff`.

source
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 = ⊥
source
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 = ⊤
source
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
source
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`

source
theorem IsCoatom.iInf_le {ι : Sort u_1} {α : Type u_2} [Order.Coframe α] {f : ι → α} {a : α} (ha : IsCoatom a) :
iInf f ≤ a ↔ ∃ (i : ι), f i ≤ a
source
@[deprecated IsCoatom.iInf_le (since := "2025-07-11")]
theorem iInf_le_coatom {ι : Sort u_1} {α : Type u_2} [Order.Coframe α] {f : ι → α} {a : α} (ha : IsCoatom a) :
iInf f ≤ a ↔ ∃ (i : ι), f i ≤ a

Alias of `IsCoatom.iInf_le`.

source
theorem IsCoatom.sInf_le {α : Type u_2} [Order.Coframe α] {s : Set α} {a : α} (ha : IsCoatom a) :
sInf s ≤ a ↔ ∃ b ∈ s, b ≤ a
source
@[simp]
theorem Set.Ici.isAtom_iff {α : Type u_2} [PartialOrder α] {a : α} {b : ↑(Ici a)} :
IsAtom b ↔ a ⋖ ↑b
source
@[simp]
theorem Set.Iic.isCoatom_iff {α : Type u_2} [PartialOrder α] {b : α} {a : ↑(Iic b)} :
IsCoatom a ↔ ↑a ⋖ b
source
theorem covBy_iff_atom_Ici {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) :
a ⋖ b ↔ IsAtom ⟨b, h⟩
source
theorem covBy_iff_coatom_Iic {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) :
a ⋖ b ↔ IsCoatom ⟨a, h⟩
source
theorem IsAtom.not_disjoint_iff_le {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) :
¬Disjoint a b ↔ a ≤ b
source
theorem IsAtom.not_le_iff_disjoint {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) :
¬a ≤ b ↔ Disjoint a b
source
theorem IsAtom.disjoint_of_ne {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) :
Disjoint a b
source
@[deprecated IsAtom.disjoint_of_ne (since := "2025-07-11")]
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 = ⊥
source
@[deprecated IsAtom.not_le_iff_disjoint (since := "2025-07-11")]
theorem IsAtom.inf_eq_bot_iff {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) :
a ⊓ b = ⊥ ↔ ¬a ≤ b
source
theorem IsCoatom.not_codisjoint_iff_le {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) :
¬Codisjoint a b ↔ b ≤ a
source
theorem IsCoatom.not_le_iff_codisjoint {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) :
¬b ≤ a ↔ Codisjoint a b
source
theorem IsCoatom.codisjoint_of_ne {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) :
Codisjoint a b
source
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 = ⊤
source
@[deprecated IsCoatom.not_le_iff_codisjoint (since := "2025-07-11")]
theorem IsCoatom.sup_eq_top_iff {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) :
a ⊔ b = ⊤ ↔ ¬b ≤ a
source
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.

Instances

source
theorem isAtomic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] :
IsAtomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
source
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.

Instances

source
theorem isCoatomic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] :
IsCoatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
source
theorem IsAtomic.exists_atom (α : Type u_2) [PartialOrder α] [OrderBot α] [Nontrivial α] [IsAtomic α] :
∃ (a : α), IsAtom a
source
theorem IsCoatomic.exists_coatom (α : Type u_2) [PartialOrder α] [OrderTop α] [Nontrivial α] [IsCoatomic α] :
∃ (a : α), IsCoatom a
source
@[simp]
theorem isCoatomic_dual_iff_isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] :
IsCoatomic α ᵒᵈ ↔ IsAtomic α
source
@[simp]
theorem isAtomic_dual_iff_isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] :
IsAtomic α ᵒᵈ ↔ IsCoatomic α
source
instance OrderDual.instIsCoatomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] :
IsCoatomic α ᵒᵈ
source
instance IsAtomic.Set.Iic.isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] {x : α} :
IsAtomic ↑(Set.Iic x)
source
instance OrderDual.instIsAtomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] :
IsAtomic α ᵒᵈ
source
instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] {x : α} :
IsCoatomic ↑(Set.Ici x)
source
theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_2} [PartialOrder α] [OrderBot α] :
IsAtomic α ↔ ∀ (x : α), IsAtomic ↑(Set.Iic x)
source
theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_2} [PartialOrder α] [OrderTop α] :
IsCoatomic α ↔ ∀ (x : α), IsCoatomic ↑(Set.Ici x)
source
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

Instances

source
theorem isStronglyAtomic_iff (α : Type u_5) [Preorder α] :
IsStronglyAtomic α ↔ ∀ (a b : α), a < b → ∃ (x : α), a ⋖ x ∧ x ≤ b
source
theorem exists_covBy_le_of_lt {α : Type u_4} {a b : α} [Preorder α] [IsStronglyAtomic α] (h : a < b) :
∃ (x : α), a ⋖ x ∧ x ≤ b
source
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`.

source
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

Instances

source
theorem isStronglyCoatomic_iff (α : Type u_5) [Preorder α] :
IsStronglyCoatomic α ↔ ∀ (a b : α), a < b → ∃ (x : α), a ≤ x ∧ x ⋖ b
source
theorem exists_le_covBy_of_lt {α : Type u_4} {a b : α} [Preorder α] [IsStronglyCoatomic α] (h : a < b) :
∃ (x : α), a ≤ x ∧ x ⋖ b
source
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`.

source
theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic {α : Type u_4} [Preorder α] :
IsStronglyAtomic α ᵒᵈ ↔ IsStronglyCoatomic α
source
@[simp]
theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic {α : Type u_4} [Preorder α] :
IsStronglyCoatomic α ᵒᵈ ↔ IsStronglyAtomic α
source
instance OrderDual.instIsStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyAtomic α] :
IsStronglyCoatomic α ᵒᵈ
source
instance instIsStronglyAtomicOrderDualOfIsStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] :
IsStronglyAtomic α ᵒᵈ
source
instance IsStronglyAtomic.isAtomic (α : Type u_5) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] :
IsAtomic α
source
instance IsStronglyCoatomic.toIsCoatomic (α : Type u_5) [PartialOrder α] [OrderTop α] [IsStronglyCoatomic α] :
IsCoatomic α
source
theorem Set.OrdConnected.isStronglyAtomic {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} (h : s.OrdConnected) :
IsStronglyAtomic ↑s
source
theorem Set.OrdConnected.isStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} (h : s.OrdConnected) :
IsStronglyCoatomic ↑s
source
instance instIsStronglyAtomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} [s.OrdConnected] :
IsStronglyAtomic ↑s
source
instance instIsStronglyCoatomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} [h : s.OrdConnected] :
IsStronglyCoatomic ↑s
source
instance SuccOrder.toIsStronglyAtomic {α : Type u_4} [Preorder α] [SuccOrder α] :
IsStronglyAtomic α
source
instance instIsStronglyCoatomicOfPredOrder {α : Type u_4} [Preorder α] [PredOrder α] :
IsStronglyCoatomic α
source
theorem IsStronglyAtomic.of_wellFounded_lt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) :
IsStronglyAtomic α
source
theorem IsStronglyCoatomic.of_wellFounded_gt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) :
IsStronglyCoatomic α
source
instance instIsStronglyAtomicOfWellFoundedLT {α : Type u_2} [PartialOrder α] [WellFoundedLT α] :
IsStronglyAtomic α
source
instance instIsStronglyCoatomicOfWellFoundedGT {α : Type u_2} [PartialOrder α] [WellFoundedGT α] :
IsStronglyCoatomic α
source
theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_2} [PartialOrder α] [OrderBot α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) :
IsAtomic α
source
theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_2} [PartialOrder α] [OrderTop α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) :
IsCoatomic α
source
theorem BooleanAlgebra.le_iff_atom_le_imp {α : Type u_4} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
source
theorem BooleanAlgebra.eq_iff_atom_le_iff {α : Type u_4} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
source
@[reducible, inline]
abbrev CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra {α : Type u_4} [CompleteBooleanAlgebra α] [IsAtomic α] :
CompleteAtomicBooleanAlgebra α

Every atomic complete Boolean algebra is completely atomic.

This is not made an instance to avoid typeclass loops.

Equations

- CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra = { toCompleteBooleanAlgebra := inst✝¹, iInf_iSup_eq := ⋯ }

Instances For

source
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.

Instances

source
theorem isAtomistic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] :
IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a
source
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.

Instances

source
theorem isCoatomistic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] :
IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a
source
@[simp]
theorem isCoatomistic_dual_iff_isAtomistic {α : Type u_2} [PartialOrder α] [OrderBot α] :
IsCoatomistic α ᵒᵈ ↔ IsAtomistic α
source
@[simp]
theorem isAtomistic_dual_iff_isCoatomistic {α : Type u_2} [PartialOrder α] [OrderTop α] :
IsAtomistic α ᵒᵈ ↔ IsCoatomistic α
source
instance OrderDual.instIsCoatomistic {α : Type u_2} [PartialOrder α] [OrderBot α] [h : IsAtomistic α] :
IsCoatomistic α ᵒᵈ
source
@[instance 100]
instance IsAtomistic.instIsAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] :
IsAtomic α
source
theorem isLUB_atoms_le {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] (b : α) :
IsLUB {a : α | IsAtom a ∧ a ≤ b} b
source
theorem isLUB_atoms_top {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] [OrderTop α] :
IsLUB {a : α | IsAtom a} ⊤
source
theorem le_iff_atom_le_imp {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} :
a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
source
theorem eq_iff_atom_le_iff {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} :
a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
source
instance OrderDual.instIsAtomistic {α : Type u_2} [PartialOrder α] [OrderTop α] [h : IsCoatomistic α] :
IsAtomistic α ᵒᵈ
source
@[instance 100]
instance IsCoatomistic.instIsCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomistic α] :
IsCoatomic α
source
@[simp]
theorem sSup_atoms_le_eq {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) :
sSup {a : α | IsAtom a ∧ a ≤ b} = b
source
@[simp]
theorem sSup_atoms_eq_top {α : Type u_4} [CompleteLattice α] [IsAtomistic α] :
sSup {a : α | IsAtom a} = ⊤
source
theorem CompleteLattice.isAtomistic_iff {α : Type u_4} [CompleteLattice α] :
IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
source
theorem eq_sSup_atoms {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) :
∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
source
theorem CompleteLattice.isCoatomistic_iff {α : Type u_4} [CompleteLattice α] :
IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
source
theorem eq_sInf_coatoms {α : Type u_4} [CompleteLattice α] [IsCoatomistic α] (b : α) :
∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
source
instance CompleteAtomicBooleanAlgebra.instIsAtomistic {α : Type u_4} [CompleteAtomicBooleanAlgebra α] :
IsAtomistic α
source
instance CompleteAtomicBooleanAlgebra.instIsCoatomistic {α : Type u_4} [CompleteAtomicBooleanAlgebra α] :
IsCoatomistic α
source
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 `⊤`

Instances

source
theorem isSimpleOrder_iff (α : Type u_4) [LE α] [BoundedOrder α] :
IsSimpleOrder α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
source
theorem IsSimpleOrder.of_forall_eq_top {α : Type u_4} [LE α] [BoundedOrder α] [Nontrivial α] (h : ∀ (a : α), a ≠ ⊥ → a = ⊤) :
IsSimpleOrder α
source
theorem isSimpleOrder_iff_isSimpleOrder_orderDual {α : Type u_2} [LE α] [BoundedOrder α] :
IsSimpleOrder α ↔ IsSimpleOrder α ᵒᵈ
source
theorem IsSimpleOrder.bot_ne_top {α : Type u_2} [LE α] [BoundedOrder α] [IsSimpleOrder α] :
⊥ ≠ ⊤
source
instance OrderDual.instIsSimpleOrder {α : Type u_4} [LE α] [BoundedOrder α] [IsSimpleOrder α] :
IsSimpleOrder α ᵒᵈ
source
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 = { toLE := inst✝², lt := fun (a b : α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

Instances For

source
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.

Instances For

source
theorem isAtom_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
IsAtom ⊤
source
@[simp]
theorem isAtom_iff_eq_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
IsAtom a ↔ a = ⊤
source
theorem isCoatom_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
IsCoatom ⊥
source
@[simp]
theorem isCoatom_iff_eq_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
IsCoatom a ↔ a = ⊥
source
theorem bot_covBy_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
⊥ ⋖ ⊤
source
theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) :
a = ⊥
source
theorem IsSimpleOrder.eq_top_of_lt {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) :
b = ⊤
source
theorem LT.lt.eq_bot {α : Type u_2} [Preorder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} (h : a < b) :
a = ⊥

Alias of `IsSimpleOrder.eq_bot_of_lt`.

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

Alias of `IsSimpleOrder.eq_top_of_lt`.

source
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

Instances For

source
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 = { toLattice := inferInstance, le_sup_inf := ⋯ }

Instances For

source
@[instance 100]
instance IsSimpleOrder.instIsAtomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] :
IsAtomic α
source
@[instance 100]
instance IsSimpleOrder.instIsCoatomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] :
IsCoatomic α
source
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 := ⋯ }

Instances For

source
@[simp]
theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : Bool) :
equivBool.symm x = Bool.casesOn x ⊥ ⊤
source
@[simp]
theorem IsSimpleOrder.equivBool_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : α) :
equivBool x = decide (x = ⊤)
source
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' := ⋯ }

Instances For

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

A simple `BoundedOrder` is also a `BooleanAlgebra`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

A simple `BoundedOrder` is also complete.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

A simple `BoundedOrder` is also a `CompleteBooleanAlgebra`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance IsSimpleOrder.instComplementedLattice {α : Type u_2} [Lattice α] [BoundedOrder α] [IsSimpleOrder α] :
ComplementedLattice α
source
@[instance 100]
instance IsSimpleOrder.instIsAtomistic {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
IsAtomistic α
source
@[instance 100]
instance IsSimpleOrder.instIsCoatomistic {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
IsCoatomistic α
source
@[simp]
theorem IsSimpleOrder.bot_lt_iff_eq_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
⊥ < a ↔ a = ⊤
source
@[simp]
theorem IsSimpleOrder.lt_top_iff_eq_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
a < ⊤ ↔ a = ⊥
source
theorem isSimpleOrder_iff_isAtom_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] :
IsSimpleOrder α ↔ IsAtom ⊤
source
theorem isSimpleOrder_iff_isCoatom_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] :
IsSimpleOrder α ↔ IsCoatom ⊥
source
theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} :
IsSimpleOrder ↑(Iic a) ↔ IsAtom a
source
theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
IsSimpleOrder ↑(Ici a) ↔ IsCoatom a
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem OrderIso.isAtom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) :
IsAtom (f a) ↔ IsAtom a
source
@[simp]
theorem OrderIso.isCoatom_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) (a : α) :
IsCoatom (f a) ↔ IsCoatom a
source
theorem OrderIso.isSimpleOrder_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) :
IsSimpleOrder α ↔ IsSimpleOrder β
source
theorem OrderIso.isSimpleOrder {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) :
IsSimpleOrder α
source
theorem OrderIso.isAtomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) :
IsAtomic α ↔ IsAtomic β
source
theorem OrderIso.isCoatomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) :
IsCoatomic α ↔ IsCoatomic β
source
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.

source
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.

source
theorem IsCompl.isAtom_iff_isCoatom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (hc : IsCompl a b) :
IsAtom a ↔ IsCoatom b
source
theorem IsCompl.isCoatom_iff_isAtom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (hc : IsCompl a b) :
IsCoatom a ↔ IsAtom b
source
theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsAtomic α] :
IsCoatomic α
source
theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsCoatomic α] :
IsAtomic α
source
theorem isAtomic_iff_isCoatomic {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] :
IsAtomic α ↔ IsCoatomic α
source
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.

source
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.

source
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.

source
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.

source
instance Prop.instIsSimpleOrderProp :
IsSimpleOrder Prop
source
theorem Prop.isAtom_iff {p : Prop} :
IsAtom p ↔ p
source
theorem Prop.isCoatom_iff {p : Prop} :
IsCoatom p ↔ ¬p
source
theorem Pi.eq_bot_iff {ι : Type u_4} {π : ι → Type u} [(i : ι) → Bot (π i)] {f : (i : ι) → π i} :
f = ⊥ ↔ ∀ (i : ι), f i = ⊥
source
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 = ⊥
source
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)
source
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
source
instance Pi.isAtomic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomic (π i)] :
IsAtomic ((i : ι) → π i)
source
instance Pi.isCoatomic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
IsCoatomic ((i : ι) → π i)
source
instance Pi.isAtomistic {ι : Type u_4} {π : ι → Type u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomistic (π i)] :
IsAtomistic ((i : ι) → π i)
source
instance Pi.isCoatomistic {ι : Type u_4} {π : ι → Type u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
IsCoatomistic ((i : ι) → π i)
source
@[simp]
theorem isAtom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} :
IsAtom a ᶜ ↔ IsCoatom a
source
@[simp]
theorem isCoatom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} :
IsCoatom a ᶜ ↔ IsAtom a
source
theorem IsCoatom.compl {α : Type u_2} [BooleanAlgebra α] {a : α} :
IsCoatom a → IsAtom a ᶜ

Alias of the reverse direction of `isAtom_compl`.

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

Alias of the forward direction of `isAtom_compl`.

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

Alias of the forward direction of `isCoatom_compl`.

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

Alias of the reverse direction of `isCoatom_compl`.

source
theorem Set.isAtom_singleton {α : Type u_2} (x : α) :
IsAtom {x}
source
theorem Set.isAtom_iff {α : Type u_2} {s : Set α} :
IsAtom s ↔ ∃ (x : α), s = {x}
source
theorem Set.isCoatom_iff {α : Type u_2} (s : Set α) :
IsCoatom s ↔ ∃ (x : α), s = {x}ᶜ
source
theorem Set.isCoatom_singleton_compl {α : Type u_2} (x : α) :
IsCoatom {x}ᶜ
source
instance Set.instIsAtomistic {α : Type u_2} :
IsAtomistic (Set α)
source
instance Set.instIsCoatomistic {α : Type u_2} :
IsCoatomistic (Set α)