Theorems · Definition · general topology
AccPt
{X : Type u_1} → [TopologicalSpace X] → X → Filter X → PropA point x is an accumulation point of a filter F if 𝓝[≠] x ⊓ F ≠ ⊥.
See also ClusterPt.
- Defined in
- Mathlib.Topology.Defs.Filter
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- Compl.complproof · cited by 2,925
- nhdsWithinproof · cited by 1,912
- Filter.NeBotproof · cited by 853
Cited by78
Results whose statement or proof uses this declaration.
- Preperfectproof · cited by 19
- derivedSetproof · cited by 16
- iteratedDerivWithin_succproof · cited by 11
- Ordinal.IsAccproof · cited by 9
- accPt_iff_clusterPtstatement · cited by 7
- AccPt.monostatement and proof · cited by 7
- accPt_principal_iff_nhdsWithinstatement · cited by 6
- fderivWithin_zero_of_not_accPtstatement and proof · cited by 6
- AccPt.clusterPtstatement and proof · cited by 6
- iteratedDerivWithin_oneproof · cited by 6
- MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithinstatement and proof · cited by 5
- uniqueDiffWithinAt_iff_accPtstatement and proof · cited by 5