Mathlib Map

Theorems · Theorem · order theory

IsAtomistic.isLUB_atoms

∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderBot α} [self : IsAtomistic α] (b : α),
  ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Every element is a sSup of a set of atoms.

Defined in
Mathlib.Order.Atoms
Cited by
4 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
IsAtomistic
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isLUB_atoms_le · cited by 3isLUB_atoms_leLattice.isStronglyAtomic · cited by 1Lattice.isStronglyAtomicisCoatomistic_dual_iff_isAtomistic · cited by 0isCoatomistic_dual_iff_is…isAtomistic_dual_iff_isCoatomistic · cited by 0isAtomistic_dual_iff_isCo…Set · cited by 53352SetPartialOrder · cited by 6410PartialOrderOrderBot · cited by 1055OrderBotIsLUB · cited by 280IsLUBIsAtom · cited by 130IsAtomIsAtomistic · cited by 18IsAtomisticIsAtomistic.isLUB_atomsCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • PartialOrderstatement and proof · cited by 6,410
  • OrderBotstatement and proof · cited by 1,055
  • IsLUBstatement · cited by 280
  • IsAtomstatement · cited by 130
  • IsAtomisticstatement and proof · cited by 18

Cited by4

Results whose statement or proof uses this declaration.