Theorems · Theorem · general topology
mem_of_mem_nhds
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, s ∈ nhds x → x ∈ s- Defined in
- Mathlib.Topology.Neighborhoods
- Cited by
- 126 results in Mathlib
- Foundations
- Depth 59 from the axioms, rests on 634 definitions · uses propext, 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
- Filterstatement · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- IsOpenproof · cited by 2,400
- mem_nhds_iffproof · cited by 67
Cited by126
Results whose statement or proof uses this declaration.
- pure_le_nhdsproof · cited by 39
- Filter.Eventually.self_of_nhdsproof · cited by 38
- ContinuousOn.continuousAtproof · cited by 33
- IsAddQuotientCoveringMap.isCoveringMapproof · cited by 16
- exists_continuous_nonneg_posproof · cited by 15
- IsQuotientCoveringMap.isCoveringMapproof · cited by 15
- ContMDiffOn.contMDiffAtproof · cited by 12
- IsOpen.mem_nhds_iffproof · cited by 10
- LocallyFinite.point_finiteproof · cited by 9
- ContDiffOn.contDiffAtproof · cited by 7
- IsOpen.pathComponentInproof · cited by 5
- AddSubgroup.isOpen_of_mem_nhdsproof · cited by 5