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) :
      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.bot_lt {α : Type u_2} [PartialOrder α] [OrderBot α] {a : α} (h : IsAtom a) :
      < 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) :
      @[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 : α} :
          @[simp]
          theorem isAtom_dual_iff_isCoatom {α : Type u_2} [Preorder α] [OrderTop α] {a : α} :
          theorem IsAtom.dual {α : Type u_2} [Preorder α] [OrderBot α] {a : α} :

          Alias of the reverse direction of isCoatom_dual_iff_isAtom.

          theorem IsCoatom.dual {α : Type u_2} [Preorder α] [OrderTop α] {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) :
          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.lt_top {α : Type u_2} [PartialOrder α] [OrderTop α] {a : α} (h : IsCoatom a) :
          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) :
          @[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 SetLike.isAtom_iff {A : Type u_4} {B : Type u_5} [SetLike A B] [OrderBot A] {K : A} :
          IsAtom K K ∀ (H : A) (g : B), H KgHg KH =
          theorem SetLike.isCoatom_iff {A : Type u_4} {B : Type u_5} [SetLike A B] [OrderTop A] {K : A} :
          IsCoatom K K ∀ (H : A) (g : B), K HgKg HH =
          theorem SetLike.covBy_iff {A : Type u_4} {B : Type u_5} [SetLike A B] {K L : A} :
          K L K < L ∀ (H : A) (g : B), K HH LgKg HH = L
          theorem SetLike.covBy_iff' {A : Type u_4} {B : Type u_5} [SetLike A B] {K L : A} :
          K L K < L ∀ (H : A) (g : B), K HH LgHg LH = K

          Dual variant of SetLike.covBy_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 : (Ici a)} :
          IsAtom b a b
          @[simp]
          theorem Set.Iic.isCoatom_iff {α : Type u_2} [PartialOrder α] {b : α} {a : (Iic b)} :
          IsCoatom a a b
          theorem covBy_iff_atom_Ici {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
          theorem covBy_iff_coatom_Iic {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
          theorem IsAtom.inf_eq_bot_of_ne {α : Type u_2} [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a b) :
          ab =
          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) :
          ab =
          theorem IsCoatom.codisjoint_of_ne {α : Type u_2} [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : 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
              instance IsAtomic.Set.Iic.isAtomic {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomic α] {x : α} :
              instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_2} [PartialOrder α] [OrderTop α] [IsCoatomic α] {x : α} :
              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.

                  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)
                  class IsAtomistic (α : Type u_2) [PartialOrder α] [OrderBot α] :

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

                  • isLUB_atoms (b : α) : ∃ (s : Set α), IsLUB s b as, IsAtom a

                    Every element is a sSup of a set of atoms.

                  Instances
                    theorem isAtomistic_iff (α : Type u_2) [PartialOrder α] [OrderBot α] :
                    IsAtomistic α ∀ (b : α), ∃ (s : Set α), IsLUB s b as, IsAtom a
                    class IsCoatomistic (α : Type u_2) [PartialOrder α] [OrderTop α] :

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

                    • isGLB_coatoms (b : α) : ∃ (s : Set α), IsGLB s b as, IsCoatom a

                      Every element is a sInf of a set of coatoms.

                    Instances
                      theorem isCoatomistic_iff (α : Type u_2) [PartialOrder α] [OrderTop α] :
                      IsCoatomistic α ∀ (b : α), ∃ (s : Set α), IsGLB s b as, IsCoatom a
                      @[instance 100]
                      theorem isLUB_atoms_le {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] (b : α) :
                      IsLUB {a : α | IsAtom a a b} b
                      theorem isLUB_atoms_top {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] [OrderTop α] :
                      theorem le_iff_atom_le_imp {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} :
                      a b ∀ (c : α), IsAtom cc ac b
                      theorem eq_iff_atom_le_iff {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] {a b : α} :
                      a = b ∀ (c : α), IsAtom c → (c a c b)
                      @[instance 100]
                      @[simp]
                      theorem sSup_atoms_le_eq {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) :
                      sSup {a : α | IsAtom a a b} = b
                      @[simp]
                      theorem sSup_atoms_eq_top {α : Type u_4} [CompleteLattice α] [IsAtomistic α] :
                      sSup {a : α | IsAtom a} =
                      theorem CompleteLattice.isAtomistic_iff {α : Type u_4} [CompleteLattice α] :
                      IsAtomistic α ∀ (b : α), ∃ (s : Set α), b = sSup s as, IsAtom a
                      theorem eq_sSup_atoms {α : Type u_4} [CompleteLattice α] [IsAtomistic α] (b : α) :
                      ∃ (s : Set α), b = sSup s as, IsAtom a
                      theorem CompleteLattice.isCoatomistic_iff {α : Type u_4} [CompleteLattice α] :
                      IsCoatomistic α ∀ (b : α), ∃ (s : Set α), b = sInf s as, IsCoatom a
                      theorem eq_sInf_coatoms {α : Type u_4} [CompleteLattice α] [IsCoatomistic α] (b : α) :
                      ∃ (s : Set α), b = sInf s as, IsCoatom a
                      class IsSimpleOrder (α : Type u_4) [LE α] [BoundedOrder α] extends Nontrivial α :

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

                      Instances
                        theorem isSimpleOrder_iff (α : Type u_4) [LE α] [BoundedOrder α] :
                        IsSimpleOrder α Nontrivial α ∀ (a : α), a = a =

                        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
                              Instances For
                                @[simp]
                                theorem isAtom_iff_eq_top {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
                                @[simp]
                                theorem isCoatom_iff_eq_bot {α : Type u_2} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a : α} :
                                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.

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

                                Equations
                                  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]
                                        @[instance 100]

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

                                        Equations
                                          Instances For
                                            @[simp]
                                            theorem IsSimpleOrder.equivBool_apply {α : Type u_4} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] (x : α) :

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

                                            Equations
                                              Instances For

                                                A simple BoundedOrder is also a BooleanAlgebra.

                                                Equations
                                                  Instances For

                                                    A simple BoundedOrder is also complete.

                                                    Equations
                                                      Instances For

                                                        A simple BoundedOrder is also a CompleteBooleanAlgebra.

                                                        Equations
                                                          Instances For
                                                            @[instance 100]
                                                            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 β) :

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

                                                            @[deprecated Lattice.isStronglyAtomic (since := "2025-03-13")]

                                                            Alias of Lattice.isStronglyAtomic.


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

                                                            A lower-modular lattice that is coatomistic is strongly coatomic. Not an instance to prevent loops.

                                                            @[deprecated Lattice.isStronglyCoatomic (since := "2025-03-13")]

                                                            Alias of Lattice.isStronglyCoatomic.


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

                                                            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)
                                                            instance Pi.isCoatomic {ι : Type u_4} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderTop (π i)] [∀ (i : ι), IsCoatomic (π i)] :
                                                            IsCoatomic ((i : ι) → π i)
                                                            instance Pi.isAtomistic {ι : Type u_4} {π : ιType u} [(i : ι) → PartialOrder (π i)] [(i : ι) → OrderBot (π i)] [∀ (i : ι), IsAtomistic (π i)] :
                                                            IsAtomistic ((i : ι) → π i)
                                                            instance Pi.isCoatomistic {ι : Type u_4} {π : ιType u} [(i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)] :
                                                            IsCoatomistic ((i : ι) → π i)
                                                            @[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 : α) :
                                                            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}
                                                            instance Set.instIsAtomistic {α : Type u_2} :