Structures · Order
IsAtomic
A lattice is atomic iff every element other than ⊥ has an atom below it.
- Defined in
- Mathlib.Order.Atoms
- Shape
- One type argument · adds eq_bot_or_exists_atom_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- LieSubmodule
- OrderDual
- Set.Elem
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- IsAtomic.eq_bot_or_exists_atom_le
- IsAtomic.exists_atom
- ComplementedLattice.isStronglyAtomic
- isCoatomic_of_isAtomic_of_complementedLattice_of_isModular
- GaloisInsertion.isAtom_iff'
- GaloisInsertion.isAtom_iff
- BooleanAlgebra.le_iff_atom_le_imp
- ComplementedLattice.isStronglyAtomic'
- GaloisCoinsertion.isAtom_iff
- CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra
- Pi.isAtomic
- IsAtomic.Set.Iic.isAtomic
- BooleanAlgebra.eq_iff_atom_le_iff
- OrderDual.instIsCoatomic
Ancestors0
No ancestors.