Theorems · Theorem · general topology
Filter.nhds_nhds
∀ {X : Type u_4} [inst : TopologicalSpace X] (x : X),
nhds (nhds x) = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal (Set.Iic (Filter.principal s))- Defined in
- Mathlib.Topology.Filter
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 66 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.
Cites14
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
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- IsOpenstatement and proof · cited by 2,400
- iInfstatement and proof · cited by 1,690
- Set.Iicstatement and proof · cited by 1,111
- CompleteLatticeproof · cited by 1,048
- Filter.principalstatement and proof · cited by 740
- nhds_basis_opensproof · cited by 54
- iInf_andproof · cited by 15
- Filter.HasBasis.eq_biInfproof · cited by 15
Cited by1
Results whose statement or proof uses this declaration.
- Filter.isInducing_nhdsproof · cited by 1