Theorems · Theorem · general topology
accPt_iff_clusterPt
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, AccPt x F ↔ ClusterPt x (Filter.principal {x}ᶜ ⊓ F)- Defined in
- Mathlib.Topology.ClusterPt
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsproof · cited by 5,554
- Compl.complstatement and proof · cited by 2,925
- Filter.NeBotproof · cited by 853
- Filter.principalstatement and proof · cited by 740
- ClusterPtstatement and proof · cited by 138
- AccPtstatement · cited by 75
- inf_assocproof · cited by 53
Cited by7
Results whose statement or proof uses this declaration.
- AccPt.clusterPtproof · cited by 6
- accPt_principal_iff_clusterPtproof · cited by 4
- hasFDerivWithinAt_singletonproof · cited by 2
- Topology.IsOpenEmbedding.accPt_comap_iffproof · cited by 2
- Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompactproof · cited by 2
- IsCountablyCompact.exists_accPt_of_infiniteproof · cited by 1
- IsOpenMap.accPt_comapproof · cited by 0