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 .

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 .

    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
          instance IsAtomic.Set.Iic.isAtomic {α : Type u_1} [PartialOrder α] [OrderBot α] [IsAtomic α] {x : α} :
          instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_1} [PartialOrder α] [OrderTop α] [IsCoatomic α] {x : α} :
          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)
          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
              @[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)
              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.

                Instances For

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

                  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

                    Instances For

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

                      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.

                        Instances For

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

                          Instances For

                            A simple BoundedOrder is also complete.

                            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)
                              instance Pi.isCoatomic {ι : Type u_3} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
                              IsCoatomic ((i : ι) → π i)
                              instance Pi.isAtomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsAtomistic (π i)] :
                              IsAtomistic ((i : ι) → π i)
                              instance Pi.isCoatomistic {ι : Type u_3} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
                              IsCoatomistic ((i : ι) → π i)
                              theorem Set.isAtom_singleton {α : Type u_1} (x : α) :
                              IsAtom {x}
                              theorem Set.isAtom_iff {α : Type u_1} (s : Set α) :
                              IsAtom s x, s = {x}
                              theorem Set.isCoatom_iff {α : Type u_1} (s : Set α) :
                              IsCoatom s x, s = {x}
                              theorem Set.isCoatom_singleton_compl {α : Type u_1} (x : α) :