Theorems · Theorem · order theory
IsAtomic.eq_bot_or_exists_atom_le
∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderBot α} [self : IsAtomic α] (b : α),
b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ bEvery element other than ⊥ has an atom below it.
- Defined in
- Mathlib.Order.Atoms
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- IsAtomic
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Bot.botstatement · cited by 4,720
- OrderBotstatement and proof · cited by 1,055
- IsAtomstatement · cited by 130
- IsAtomicstatement and proof · cited by 20
Cited by12
Results whose statement or proof uses this declaration.
- IsAtomic.exists_atomproof · cited by 4
- IsSemisimpleModule.eq_bot_or_exists_simple_leproof · cited by 4
- isCoatomic_dual_iff_isAtomicproof · cited by 3
- ComplementedLattice.isStronglyAtomicproof · cited by 2
- Ultrafilter.exists_leproof · cited by 2
- isCoatomic_of_isAtomic_of_complementedLattice_of_isModularproof · cited by 2
- isAtomic_dual_iff_isCoatomicproof · cited by 2
- GaloisInsertion.isAtom_iffproof · cited by 2
- LieAlgebra.InvariantForm.atomisticproof · cited by 1
- BooleanAlgebra.le_iff_atom_le_impproof · cited by 1
- isAtomic_iff_forall_isAtomic_Iicproof · cited by 1
- CategoryTheory.exists_simple_subobjectproof · cited by 0