Theorems · Theorem · general topology
mem_closure_iff_nhds_basis
∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X},
(nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i)- Defined in
- Mathlib.Topology.ClusterPt
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- nhdsstatement and proof · cited by 5,554
- closurestatement · cited by 1,254
- Filter.HasBasisstatement and proof · cited by 604
- mem_closure_iff_nhds_basis'proof · cited by 3
Cited by13
Results whose statement or proof uses this declaration.
- Metric.mem_closure_iffproof · cited by 18
- EMetric.mem_closure_iffproof · cited by 6
- SchwartzMap.denseRange_toLpCLMproof · cited by 3
- closure_eq_uniformityproof · cited by 2
- MeasureTheory.Lp.boundedContinuousFunction_denseproof · cited by 2
- mem_closure_iff_nhds_zeroproof · cited by 1
- Real.mem_closure_iffproof · cited by 1
- ContinuousMap.dense_setOfPred_contDiffproof · cited by 1
- mem_closure_iff_nhds_oneproof · cited by 0
- MeasureTheory.Lp.dense_hasCompactSupport_contDiffproof · cited by 0
- UniformSpace.mem_closure_iff_symm_ballproof · cited by 0
- Filter.HasBasis.biInter_biUnion_ballproof · cited by 0