Mathlib Map

Theorems · Definition · order theory

IsAtom

{α : Type u_2} → [inst : Preorder α] → [OrderBot α] → α → Prop

An atom of an OrderBot is an element with no other element between it and ⊥, which is not ⊥.

Defined in
Mathlib.Order.Atoms
Cited by
130 results in Mathlib
Foundations
Depth 3 from the axioms, rests on 16 definitions · uses no axioms
Assumes
PreorderOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

OrderIso.isSimpleOrder_iff · cited by 12OrderIso.isSimpleOrder_iffIsAtomic.eq_bot_or_exists_atom_le · cited by 12IsAtomic.eq_bot_or_exists…IsAtom.le_iff · cited by 10IsAtom.le_iffIsAtom.le_iff_eq · cited by 8IsAtom.le_iff_eqisSimpleModule_iff_isAtom · cited by 7isSimpleModule_iff_isAtomIsCoatom.dual · cited by 6IsCoatom.dualIsCompactlyGenerated.BooleanGenerators.isAtom · cited by 6BooleanGenerators.isAtomOrderIso.isAtom_iff · cited by 5OrderIso.isAtom_iffisAtom_top · cited by 5isAtom_topIsAtom.lt_iff · cited by 5IsAtom.lt_iffbot_covBy_iff · cited by 4bot_covBy_iffIsSemisimpleModule.eq_bot_or_exists_simple_le · cited by 4IsSemisimpleModule.eq_bot…RootedTree.subtrees · cited by 4RootedTree.subtreesIsAtomic.exists_atom · cited by 4IsAtomic.exists_atomIsAtomistic.isLUB_atoms · cited by 4IsAtomistic.isLUB_atomsPreorder · cited by 7952PreorderBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotIsAtomCITED BYCITES

Cites3

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

  • Preorderstatement and proof · cited by 7,952
  • Bot.botproof · cited by 4,720
  • OrderBotstatement and proof · cited by 1,055

Cited by142

Results whose statement or proof uses this declaration.