Theorems · Theorem · general topology
accPt_principal_iff_nhdsWithin
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
AccPt x (Filter.principal s) ↔ (nhdsWithin x (s \ {x})).NeBot- Defined in
- Mathlib.Topology.ClusterPt
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- TopologicalSpacestatement and proof · cited by 24,529
- Filterproof · cited by 8,121
- nhdsproof · cited by 5,554
- nhdsWithinstatement and proof · cited by 1,912
- Filter.NeBotstatement and proof · cited by 853
- Filter.principalstatement and proof · cited by 740
- AccPtstatement · cited by 75
- accPt_principal_iff_clusterPtproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- HasDerivWithinAt.nonneg_of_monotoneOnproof · cited by 4
- MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAtproof · cited by 3
- HasFDerivWithinAt.of_not_accPtproof · cited by 3
- range_derivWithin_subset_closure_span_imageproof · cited by 3
- Complex.derivWithin_const_cpowproof · cited by 1
- perfectSpace_of_moduleproof · cited by 0