Mathlib Map

Theorems · Definition · general topology

Ultrafilter.ofAtom

{α : Type u} → (f : Filter α) → IsAtom f → Ultrafilter α

If f : Filter α is an atom, then it is an ultrafilter.

Defined in
Mathlib.Order.Filter.Ultrafilter.Defs
Cited by
1 results in Mathlib
Foundations
Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ultrafilter.exists_le · cited by 2Ultrafilter.exists_leFilter · cited by 8121FilterUltrafilter · cited by 193UltrafilterIsAtom · cited by 130IsAtomUltrafilter.ofAtomCITED BYCITES

Cites3

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

  • Filterstatement and proof · cited by 8,121
  • Ultrafilterstatement · cited by 193
  • IsAtomstatement and proof · cited by 130

Cited by1

Results whose statement or proof uses this declaration.