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

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

Equations
Instances For
    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 aa 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 : α} :
    theorem Covby.is_atom {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
    aIsAtom 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 : α) :

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

    Equations
    Instances For
      @[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 aIsCoatom (OrderDual.toDual a)

      Alias of the reverse direction of isCoatom_dual_iff_isAtom.

      theorem IsCoatom.dual {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
      IsCoatom aIsAtom (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) :
      theorem isCoatom_iff {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
      IsCoatom a a ∀ (b : α), b a bb 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 : α} :
      theorem IsCoatom.covby_top {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
      IsCoatom aa

      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) :
      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 α] :
      • 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.

      Instances
        theorem IsCoatomic_iff (α : Type u_1) [PartialOrder α] [OrderTop α] :
        IsCoatomic α ∀ (b : α), b = a, IsCoatom a b a
        class IsCoatomic (α : Type u_1) [PartialOrder α] [OrderTop α] :
        • 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.

        Instances
          theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_1} [PartialOrder α] [OrderBot α] :
          IsAtomic α ∀ (x : α), IsAtomic ↑(Set.Iic x)
          theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [PartialOrder α] [OrderBot α] (h : WellFounded fun x x_1 => x < x_1) :
          theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [PartialOrder α] [OrderTop α] (h : WellFounded fun x x_1 => x > x_1) :
          theorem BooleanAlgebra.le_iff_atom_le_imp {α : Type u_3} [BooleanAlgebra α] [IsAtomic α] {x : α} {y : α} :
          x y ∀ (a : α), IsAtom aa xa 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]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            class IsAtomistic (α : Type u_1) [CompleteLattice α] :
            • eq_sSup_atoms : ∀ (b : α), s, b = sSup s ∀ (a : α), a sIsAtom 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.

            Instances
              class IsCoatomistic (α : Type u_1) [CompleteLattice α] :
              • eq_sInf_coatoms : ∀ (b : α), s, b = sInf s ∀ (a : α), a sIsCoatom 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.

              Instances
                Equations
                • One or more equations did not get rendered due to their size.
                @[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 cc ac b
                theorem eq_iff_atom_le_iff {α : Type u_1} [CompleteLattice α] [IsAtomistic α] {a : α} {b : α} :
                a = b ∀ (c : α), IsAtom c → (c a c b)
                Equations
                • One or more equations did not get rendered due to their size.
                class IsSimpleOrder (α : Type u_3) [LE α] [BoundedOrder α] extends Nontrivial :
                • 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 .

                Instances

                  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)
                  Instances For

                    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
                      @[simp]
                      theorem isAtom_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
                      @[simp]
                      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.

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

                      Equations
                      • IsSimpleOrder.lattice = LinearOrder.toLattice
                      Instances For

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

                        Equations
                        Instances For
                          @[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 = )

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

                              A simple BoundedOrder is also a BooleanAlgebra.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                A simple BoundedOrder is also complete.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  A simple BoundedOrder is also a CompleteBooleanAlgebra.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    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)) :
                                    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)) :
                                    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)) :
                                    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 au (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 au (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)) :
                                    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 au (l a) = a) (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)) :
                                    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 bl (u b) = b) (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 bl (u b) = b) (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)) :
                                    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 bl (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 {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) :
                                    theorem OrderIso.isAtomic_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) :
                                    theorem OrderIso.isCoatomic_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) :
                                    theorem IsCompl.isAtom_iff_isCoatom {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a : α} {b : α} (hc : IsCompl a b) :
                                    theorem IsCompl.isCoatom_iff_isAtom {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a : α} {b : α} (hc : IsCompl a b) :
                                    @[simp]
                                    theorem Prop.isAtom_iff {p : Prop} :
                                    @[simp]
                                    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 if j =
                                    theorem Pi.isAtom_single {ι : Type u_3} {π : ιType u} {i : ι} [DecidableEq ι] [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] {a : π i} (h : IsAtom 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)
                                    Equations
                                    instance Pi.isCoatomic {ι : Type u_3} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
                                    IsCoatomic ((i : ι) → π i)
                                    Equations
                                    instance Pi.isAtomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsAtomistic (π i)] :
                                    IsAtomistic ((i : ι) → π i)
                                    Equations
                                    instance Pi.isCoatomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
                                    IsCoatomistic ((i : ι) → π i)
                                    Equations
                                    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.