Theorems · Inductive type · order theory
IsAtomistic
(α : Type u_2) → [inst : PartialOrder α] → [OrderBot α] → Prop
A lattice is atomistic iff every element is a sSup of a set of atoms.
- Defined in
- Mathlib.Order.Atoms
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- PartialOrderOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement · cited by 6,410
- OrderBotstatement · cited by 1,055
Cited by20
Results whose statement or proof uses this declaration.
- IsAtomistic.isLUB_atomsstatement and proof · cited by 4
- isLUB_atoms_lestatement and proof · cited by 3
- CompleteLattice.isAtomistic_iffstatement · cited by 2
- complementedLattice_of_isAtomisticstatement and proof · cited by 2
- sSup_atoms_eq_topstatement and proof · cited by 2
- eq_sSup_atomsstatement and proof · cited by 1
- complementedLattice_iff_isAtomisticstatement and proof · cited by 1
- complementedLattice_of_complementedLattice_Iicproof · cited by 1
- le_iff_atom_le_impstatement and proof · cited by 1
- sSup_atoms_le_eqstatement and proof · cited by 1
- Lattice.isStronglyAtomicstatement and proof · cited by 1
- IsAtomistic.casesOnstatement and proof · cited by 1