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_1} [inst : Preorder α] [inst : 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_1} [inst : Preorder α] [inst : OrderBot α] {a : α} {x : α} (ha : IsAtom a) (hax : a x) :
IsAtom { val := a, property := hax }
theorem IsAtom.of_isAtom_coe_Iic {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {x : α} {a : ↑(Set.Iic x)} (ha : IsAtom a) :
IsAtom a
theorem isAtom_iff {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :
IsAtom a a ∀ (b : α), b b aa b
theorem IsAtom.lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {x : α} (h : IsAtom a) :
x < a x =
theorem IsAtom.le_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {x : α} (h : IsAtom a) :
x a x = x = a
theorem IsAtom.Iic_eq {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} (h : IsAtom a) :
Set.Iic a = {, a}
@[simp]
theorem bot_covby_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
theorem Covby.is_atom {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
aIsAtom a

Alias of the forward direction of bot_covby_iff.

theorem IsAtom.bot_covby {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
IsAtom a a

Alias of the reverse direction of bot_covby_iff.

def IsCoatom {α : Type u_1} [inst : Preorder α] [inst : 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_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :
IsCoatom (OrderDual.toDual a) IsAtom a
@[simp]
theorem isAtom_dual_iff_isCoatom {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :
IsAtom (OrderDual.toDual a) IsCoatom a
theorem IsAtom.dual {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :
IsAtom aIsCoatom (OrderDual.toDual a)

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

theorem IsCoatom.dual {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :
IsCoatom aIsAtom (OrderDual.toDual a)

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

theorem IsCoatom.Ici {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} {x : α} (ha : IsCoatom a) (hax : x a) :
IsCoatom { val := a, property := hax }
theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {x : α} {a : ↑(Set.Ici x)} (ha : IsCoatom a) :
theorem isCoatom_iff {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :
IsCoatom a a ∀ (b : α), b a bb a
theorem IsCoatom.lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {x : α} (h : IsCoatom a) :
a < x x =
theorem IsCoatom.le_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {x : α} (h : IsCoatom a) :
a x x = x = a
theorem IsCoatom.Ici_eq {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : IsCoatom a) :
Set.Ici a = {, a}
@[simp]
theorem covby_top_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
theorem Covby.is_coatom {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
a IsCoatom a

Alias of the forward direction of covby_top_iff.

theorem IsCoatom.covby_top {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
IsCoatom aa

Alias of the reverse direction of covby_top_iff.

@[simp]
theorem Set.Ici.isAtom_iff {α : Type u_1} [inst : PartialOrder α] {a : α} {b : ↑(Set.Ici a)} :
IsAtom b a b
@[simp]
theorem Set.Iic.isCoatom_iff {α : Type u_1} [inst : PartialOrder α] {b : α} {a : ↑(Set.Iic b)} :
IsCoatom a a b
theorem covby_iff_atom_Ici {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a b IsAtom { val := b, property := h }
theorem covby_iff_coatom_Iic {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a b IsCoatom { val := a, property := h }
theorem IsAtom.inf_eq_bot_of_ne {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a b) :
a b =
theorem IsAtom.disjoint_of_ne {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a b) :
theorem IsCoatom.sup_eq_top_of_ne {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a b) :
a b =
theorem IsAtomic_iff (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] :
IsAtomic α ∀ (b : α), b = a, IsAtom a a b
class IsAtomic (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] :
  • Every element other than has an atom below it.

    eq_bot_or_exists_atom_le : ∀ (b : α), b = a, IsAtom a a b

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

Instances
    theorem IsCoatomic_iff (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] :
    IsCoatomic α ∀ (b : α), b = a, IsCoatom a b a
    class IsCoatomic (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] :
    • Every element other than has an atom above it.

      eq_top_or_exists_le_coatom : ∀ (b : α), b = a, IsCoatom a b a

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

    Instances
      @[simp]
      theorem isCoatomic_dual_iff_isAtomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :
      @[simp]
      theorem isAtomic_dual_iff_isCoatomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :
      theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :
      IsAtomic α ∀ (x : α), IsAtomic ↑(Set.Iic x)
      theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :
      IsCoatomic α ∀ (x : α), IsCoatomic ↑(Set.Ici x)
      theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] (h : WellFounded fun x x_1 => x < x_1) :
      theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] (h : WellFounded fun x x_1 => x > x_1) :
      class IsAtomistic (α : Type u_1) [inst : CompleteLattice α] :
      • Every element is a supₛ of a set of atoms.

        eq_supₛ_atoms : ∀ (b : α), s, b = supₛ s ∀ (a : α), a sIsAtom a

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

      Instances
        class IsCoatomistic (α : Type u_1) [inst : CompleteLattice α] :
        • Every element is a infₛ of a set of coatoms.

          eq_infₛ_coatoms : ∀ (b : α), s, b = infₛ s ∀ (a : α), a sIsCoatom a

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

        Instances
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem supₛ_atoms_le_eq {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] (b : α) :
          supₛ { a | IsAtom a a b } = b
          @[simp]
          theorem supₛ_atoms_eq_top {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] :
          supₛ { a | IsAtom a } =
          theorem le_iff_atom_le_imp {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] {a : α} {b : α} :
          a b ∀ (c : α), IsAtom cc ac b
          Equations
          • One or more equations did not get rendered due to their size.
          class IsSimpleOrder (α : Type u_1) [inst : LE α] [inst : BoundedOrder α] extends Nontrivial :
          • Every element is either or

            eq_bot_or_eq_top : ∀ (a : α), a = a =

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

          Instances
            theorem IsSimpleOrder.bot_ne_top {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :
            def IsSimpleOrder.preorder {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

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

            Equations
            • IsSimpleOrder.preorder = Preorder.mk (_ : ∀ (a : α), a a) (_ : ∀ (a b c : α), a bb ca c)
            def IsSimpleOrder.linearOrder {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] [inst : DecidableEq α] :

            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_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :
            @[simp]
            theorem isCoatom_bot {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :
            theorem bot_covby_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :
            theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :
            a =
            theorem IsSimpleOrder.eq_top_of_lt {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :
            b =
            theorem IsSimpleOrder.LT.lt.eq_bot {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :
            a =

            Alias of IsSimpleOrder.eq_bot_of_lt.

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

            Alias of IsSimpleOrder.eq_top_of_lt.

            def IsSimpleOrder.lattice {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

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

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

            Equations
            @[simp]
            theorem IsSimpleOrder.equivBool_apply {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] (x : α) :
            IsSimpleOrder.equivBool x = decide (x = )
            @[simp]
            theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] (x : Bool) :
            ↑(Equiv.symm IsSimpleOrder.equivBool) x = bif x then else
            def IsSimpleOrder.equivBool {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

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

            Equations
            • One or more equations did not get rendered due to their size.
            def IsSimpleOrder.orderIsoBool {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

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

            Equations
            • One or more equations did not get rendered due to their size.
            def IsSimpleOrder.booleanAlgebra {α : Type u_1} [inst : DecidableEq α] [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

            A simple BoundedOrder is also a BooleanAlgebra.

            Equations
            • One or more equations did not get rendered due to their size.
            noncomputable def IsSimpleOrder.completeLattice {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

            A simple BoundedOrder is also complete.

            Equations
            • One or more equations did not get rendered due to their size.
            noncomputable def IsSimpleOrder.completeBooleanAlgebra {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

            A simple BoundedOrder is also a CompleteBooleanAlgebra.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
            theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
            theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] (f : β ↪o α) (hbot : f.toEmbedding = ) {b : β} (hb : IsAtom (f.toEmbedding b)) :
            theorem OrderEmbedding.isCoatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] (f : β ↪o α) (htop : f.toEmbedding = ) {b : β} (hb : IsCoatom (f.toEmbedding b)) :
            theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] {l : αβ} {u : βα} (gi : GaloisInsertion l u) (hbot : u = ) {b : β} (hb : IsAtom (u b)) :
            theorem GaloisInsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : IsAtomic α] [inst : 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_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : IsAtomic α] [inst : 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_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] {l : αβ} {u : βα} (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) :
            theorem GaloisInsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : IsCoatomic α] [inst : OrderTop β] {l : αβ} {u : βα} (gi : GaloisInsertion l u) (h_coatom : ∀ (a : α), IsCoatom au (l a) = a) (b : β) :
            theorem GaloisCoinsertion.isCoatom_of_l_top {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] {l : αβ} {u : βα} (gi : GaloisCoinsertion l u) (hbot : l = ) {a : α} (hb : IsCoatom (l a)) :
            theorem GaloisCoinsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] [inst : IsCoatomic β] {l : αβ} {u : βα} (gi : GaloisCoinsertion l u) (htop : l = ) (h_coatom : ∀ (b : β), IsCoatom bl (u b) = b) (b : β) :
            theorem GaloisCoinsertion.isCoatom_iff' {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] [inst : 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_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] {l : αβ} {u : βα} (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) :
            theorem GaloisCoinsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] [inst : 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_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] (f : α ≃o β) (a : α) :
            IsAtom ((RelIso.toRelEmbedding f).toEmbedding a) IsAtom a
            @[simp]
            theorem OrderIso.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] (f : α ≃o β) (a : α) :
            IsCoatom ((RelIso.toRelEmbedding f).toEmbedding a) IsCoatom a
            theorem OrderIso.isSimpleOrder_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : α ≃o β) :
            theorem OrderIso.isSimpleOrder {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : BoundedOrder α] [inst : BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) :
            theorem OrderIso.isAtomic_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] (f : α ≃o β) :
            theorem OrderIso.isCoatomic_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] (f : α ≃o β) :
            theorem IsCompl.isAtom_iff_isCoatom {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsModularLattice α] {a : α} {b : α} (hc : IsCompl a b) :
            theorem IsCompl.isCoatom_iff_isAtom {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsModularLattice α] {a : α} {b : α} (hc : IsCompl a b) :
            theorem isAtomic_iff_isCoatomic {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsModularLattice α] [inst : ComplementedLattice α] :
            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 : α) :
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.