Documentation

Mathlib.Order.Atoms

Atoms, Coatoms, and Simple Lattices #

This module defines atoms, which are minimal non- elements in bounded lattices, simple lattices, which are lattices with only two elements, and related ideas.

Main definitions #

Atoms and Coatoms #

Atomic and Atomistic Lattices #

Simple Lattices #

Main results #

def IsAtom {α : Type u_2} [Preorder α] [OrderBot α] (a : α) :

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

Equations
theorem IsAtom.Iic {α : Type u_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 aa 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.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 : α} :
theorem CovBy.is_atom {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} :
aIsAtom 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 : α) :

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

Equations
@[simp]
theorem isCoatom_dual_iff_isAtom {α : Type u_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 aIsCoatom (OrderDual.toDual a)

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

theorem IsCoatom.dual {α : Type u_2} [Preorder α] [OrderTop α] {a : α} :
IsCoatom aIsAtom (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) :
theorem isCoatom_iff_ge_of_le {α : Type u_2} [Preorder α] [OrderTop α] {a : α} :
IsCoatom a a ∀ (b : α), b a bb 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.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 : α} :
theorem CovBy.isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
a IsCoatom a

Alias of the forward direction of covBy_top_iff.

theorem IsCoatom.covBy_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
IsCoatom aa

Alias of the reverse direction of covBy_top_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 : (Set.Ici a)} :
IsAtom b a b
@[simp]
theorem Set.Iic.isCoatom_iff {α : Type u_2} [PartialOrder α] {b : α} {a : (Set.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) :
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 =
class IsAtomic (α : Type u_2) [PartialOrder α] [OrderBot α] :

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
theorem isAtomic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] :
IsAtomic α ∀ (b : α), b = ∃ (a : α), IsAtom a a b
class IsCoatomic (α : Type u_2) [PartialOrder α] [OrderTop α] :

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
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
Equations
  • =
instance IsAtomic.Set.Iic.isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] {x : α} :
Equations
  • =
Equations
  • =
instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] {x : α} :
Equations
  • =
theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_2} [PartialOrder α] [OrderBot α] :
IsAtomic α ∀ (x : α), IsAtomic (Set.Iic x)
class IsStronglyAtomic (α : Type u_5) [Preorder α] :

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
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 α] :

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

Equations
  • =
Equations
  • =
theorem Set.OrdConnected.isStronglyAtomic {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} (h : s.OrdConnected) :
theorem Set.OrdConnected.isStronglyCoatomic {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} (h : s.OrdConnected) :
instance instIsStronglyAtomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyAtomic α] {s : Set α} [s.OrdConnected] :
Equations
  • =
instance instIsStronglyCoatomicElemOfOrdConnected {α : Type u_4} [Preorder α] [IsStronglyCoatomic α] {s : Set α} [h : s.OrdConnected] :
Equations
  • =
Equations
  • =
Equations
  • =
theorem IsStronglyAtomic.of_wellFounded_lt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) :
theorem IsStronglyCoatomic.of_wellFounded_gt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) :
theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_2} [PartialOrder α] [OrderBot α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) :
theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_2} [PartialOrder α] [OrderTop α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) :
theorem BooleanAlgebra.le_iff_atom_le_imp {α : Type u_4} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
x y ∀ (a : α), IsAtom aa xa 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]
Equations
class IsAtomistic (α : Type u_2) [CompleteLattice α] :

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

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

    Every element is a sSup of a set of atoms.

Instances
class IsCoatomistic (α : Type u_2) [CompleteLattice α] :

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

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

    Every element is a sInf of a set of coatoms.

Instances
Equations
  • =
@[instance 100]
Equations
  • =
@[simp]
theorem sSup_atoms_le_eq {α : Type u_2} [CompleteLattice α] [IsAtomistic α] (b : α) :
sSup {a : α | IsAtom a a b} = b
@[simp]
theorem sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsAtomistic α] :
sSup {a : α | IsAtom a} =
theorem le_iff_atom_le_imp {α : Type u_2} [CompleteLattice α] [IsAtomistic α] {a b : α} :
a b ∀ (c : α), IsAtom cc ac b
theorem eq_iff_atom_le_iff {α : Type u_2} [CompleteLattice α] [IsAtomistic α] {a b : α} :
a = b ∀ (c : α), IsAtom c(c a c b)
Equations
  • =
@[instance 100]
Equations
  • =
Equations
  • =

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

Equations

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 α] :
@[simp]
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.

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

Alias of IsSimpleOrder.eq_bot_of_lt.


Alias of IsSimpleOrder.eq_bot_of_lt.

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

Alias of IsSimpleOrder.eq_top_of_lt.


Alias of IsSimpleOrder.eq_top_of_lt.

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

Equations
  • IsSimpleOrder.lattice = LinearOrder.toLattice

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

Equations
@[instance 100]
Equations
  • =
@[instance 100]
Equations
  • =

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

Equations
@[simp]
theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : Bool) :
IsSimpleOrder.equivBool.symm x = Bool.casesOn x
@[simp]
theorem IsSimpleOrder.equivBool_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : α) :
IsSimpleOrder.equivBool x = decide (x = )

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

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

A simple BoundedOrder is also a BooleanAlgebra.

Equations

A simple BoundedOrder is also complete.

Equations

A simple BoundedOrder is also a CompleteBooleanAlgebra.

Equations
@[instance 100]
Equations
  • =
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)) :
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)) :
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)) :
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 au (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 au (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)) :
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 au (l a) = a) (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)) :
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 bl (u b) = b) (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 bl (u b) = b) (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)) :
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 bl (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 : α) :
theorem OrderIso.isSimpleOrder {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) :
theorem OrderIso.isAtomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) :
theorem OrderIso.isCoatomic_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) :

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

A complete 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) :
theorem IsCompl.isCoatom_iff_isAtom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b : α} (hc : IsCompl a b) :

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

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

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

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

@[simp]
theorem Prop.isAtom_iff {p : Prop} :
@[simp]
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 if j =
theorem Pi.isAtom_single {ι : Type u_4} {π : ιType u} {i : ι} [DecidableEq ι] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {a : π i} (h : IsAtom 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)
Equations
  • =
instance Pi.isCoatomic {ι : Type u_4} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
IsCoatomic ((i : ι) → π i)
Equations
  • =
instance Pi.isAtomistic {ι : Type u_4} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsAtomistic (π i)] :
IsAtomistic ((i : ι) → π i)
Equations
  • =
instance Pi.isCoatomistic {ι : Type u_4} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
IsCoatomistic ((i : ι) → π i)
Equations
  • =
@[simp]
theorem isAtom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} :
@[simp]
theorem isCoatom_compl {α : Type u_2} [BooleanAlgebra α] {a : α} :
theorem IsCoatom.compl {α : Type u_2} [BooleanAlgebra α] {a : α} :

Alias of the reverse direction of isAtom_compl.

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

Alias of the forward direction of isAtom_compl.

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

Alias of the reverse direction of isCoatom_compl.

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

Alias of the forward 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 : α) :
instance Set.instIsAtomistic {α : Type u_2} :
Equations
  • =
instance Set.instIsCoatomistic {α : Type u_2} :
Equations
  • =