Theorems · Inductive type · order theory
IsAtomic
(α : Type u_2) → [inst : PartialOrder α] → [OrderBot α] → Prop
A lattice is atomic iff every element other than ⊥ has an atom below it.
- Defined in
- Mathlib.Order.Atoms
- Cited by
- 20 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 by23
Results whose statement or proof uses this declaration.
- IsAtomic.eq_bot_or_exists_atom_lestatement and proof · cited by 12
- IsAtomic.exists_atomstatement and proof · cited by 4
- isCoatomic_dual_iff_isAtomicstatement and proof · cited by 3
- ComplementedLattice.isStronglyAtomicstatement and proof · cited by 2
- isAtomic_dual_iff_isCoatomicstatement and proof · cited by 2
- isCoatomic_of_isAtomic_of_complementedLattice_of_isModularstatement and proof · cited by 2
- GaloisInsertion.isAtom_iffstatement and proof · cited by 2
- GaloisInsertion.isAtom_iff'statement and proof · cited by 2
- BooleanAlgebra.le_iff_atom_le_impstatement and proof · cited by 1
- isAtomic_iff_forall_isAtomic_Iicstatement and proof · cited by 1
- isAtomic_of_isCoatomic_of_complementedLattice_of_isModularstatement · cited by 1
- isAtomic_of_orderBot_wellFounded_ltstatement · cited by 1