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
Instances For
    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
    Instances For
      @[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 IsCoatom.covBy_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
      IsCoatom aa

      Alias of the reverse direction of covBy_top_iff.

      theorem CovBy.isCoatom {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} :
      a IsCoatom a

      Alias of the forward 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 =
      theorem isAtomic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] :
      IsAtomic α ∀ (b : α), b = ∃ (a : α), IsAtom a 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.eq_bot_or_exists_atom_le {α : Type u_2} [PartialOrder α] [OrderBot α] [self : IsAtomic α] (b : α) :
        b = ∃ (a : α), IsAtom a a b

        Every element other than has an atom below it.

        theorem isCoatomic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] :
        IsCoatomic α ∀ (b : α), b = ∃ (a : α), IsCoatom a b a
        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.eq_top_or_exists_le_coatom {α : Type u_2} [PartialOrder α] [OrderTop α] [self : IsCoatomic α] (b : α) :
          b = ∃ (a : α), IsCoatom a b a

          Every element other than has an atom above it.

          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)
          theorem isStronglyAtomic_iff (α : Type u_5) [Preorder α] :
          IsStronglyAtomic α ∀ (a b : α), a < b∃ (x : α), a x x b
          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.exists_covBy_le_of_lt {α : Type u_5} [Preorder α] [self : 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.

            theorem isStronglyCoatomic_iff (α : Type u_5) [Preorder α] :
            IsStronglyCoatomic α ∀ (a b : α), a < b∃ (x : α), a x x b
            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.exists_le_covBy_of_lt {α : Type u_5} [Preorder α] [self : 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 (x x_1 : α) => x < x_1) :
              theorem IsStronglyCoatomic.of_wellFounded_gt {α : Type u_2} [PartialOrder α] (h : WellFounded fun (x x_1 : α) => x > x_1) :
              theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_2} [PartialOrder α] [OrderBot α] (h : WellFounded fun (x x_1 : α) => x < x_1) :
              theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_2} [PartialOrder α] [OrderTop α] (h : WellFounded fun (x x_1 : α) => x > x_1) :
              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
              Instances For
                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
                  theorem IsAtomistic.eq_sSup_atoms {α : Type u_2} [CompleteLattice α] [self : IsAtomistic α] (b : α) :
                  ∃ (s : Set α), b = sSup s as, IsAtom a

                  Every element is a sSup of a set of atoms.

                  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
                    theorem IsCoatomistic.eq_sInf_coatoms {α : Type u_2} [CompleteLattice α] [self : IsCoatomistic α] (b : α) :
                    ∃ (s : Set α), b = sInf s as, IsCoatom a

                    Every element is a sInf of a set of coatoms.

                    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
                    • =
                    class IsSimpleOrder (α : Type u_4) [LE α] [BoundedOrder α] extends Nontrivial :

                    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
                      theorem IsSimpleOrder.eq_bot_or_eq_top {α : Type u_4} [LE α] [BoundedOrder α] [self : IsSimpleOrder α] (a : α) :
                      a = a =

                      Every element is either or

                      Equations
                      • =

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

                      Equations
                      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_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
                          Instances For

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

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

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

                              Equations
                              Instances For

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

                                Equations
                                • IsSimpleOrder.orderIsoBool = let __src := IsSimpleOrder.equivBool; { toEquiv := __src, map_rel_iff' := }
                                Instances For

                                  A simple BoundedOrder is also a BooleanAlgebra.

                                  Equations
                                  Instances For

                                    A simple BoundedOrder is also complete.

                                    Equations
                                    • IsSimpleOrder.completeLattice = let __src := inferInstance; let __src_1 := inferInstance; CompleteLattice.mk
                                    Instances For

                                      A simple BoundedOrder is also a CompleteBooleanAlgebra.

                                      Equations
                                      • IsSimpleOrder.completeBooleanAlgebra = let __spread.0 := IsSimpleOrder.completeLattice; let __spread.1 := IsSimpleOrder.booleanAlgebra; CompleteBooleanAlgebra.mk
                                      Instances For
                                        @[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 IsCoatom.of_compl {α : Type u_2} [BooleanAlgebra α] {a : α} :

                                        Alias of the forward direction of isCoatom_compl.

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

                                        Alias of the reverse 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
                                        • =