Theorems · Theorem · general topology
Filter.principal_singleton
∀ {α : Type u_1} (a : α), Filter.principal {a} = pure a- Defined in
- Mathlib.Order.Filter.Map
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Filterstatement · cited by 8,121
- Filter.principalstatement · cited by 740
- Filter.extproof · cited by 60
Cited by31
Results whose statement or proof uses this declaration.
- isCompact_singletonproof · cited by 32
- nhdsWithin_singletonproof · cited by 12
- TendstoLocallyUniformlyOn.tendsto_atproof · cited by 11
- Filter.le_pure_iffproof · cited by 11
- specializes_TFAEproof · cited by 6
- Filter.OrderBot.atBot_eqproof · cited by 4
- Filter.OrderTop.atTop_eqproof · cited by 4
- isLindelof_singletonproof · cited by 4
- Filter.comap_pureproof · cited by 3
- TendstoUniformlyOnFilter.tendsto_atproof · cited by 3
- tendsto_indicator_const_apply_iff_eventually'proof · cited by 2
- Filter.smallSets_botproof · cited by 2