Theorems · Theorem · general topology
mem_nhds_iff
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t- Defined in
- Mathlib.Topology.Neighborhoods
- Cited by
- 67 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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 · cited by 5,554
- IsOpenstatement and proof · cited by 2,400
- Filter.HasBasis.mem_iffproof · cited by 193
- nhds_basis_opensproof · cited by 54
Cited by67
Results whose statement or proof uses this declaration.
- IsOpen.mem_nhdsproof · cited by 470
- mem_of_mem_nhdsproof · cited by 126
- mem_interior_iff_mem_nhdsproof · cited by 82
- eventually_nhds_iffproof · cited by 21
- IsOpen.mem_nhds_iffproof · cited by 10
- IsOpenMap.image_mem_nhdsproof · cited by 10
- isMIntegralCurveAt_iffproof · cited by 7
- StructureGroupoid.LocalInvariantProp.congr_setproof · cited by 5
- ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_oneproof · cited by 5
- isIntegralCurveAt_iff_exists_mem_nhdsproof · cited by 5
- TopologicalSpace.nhds_mkOfNhds_of_hasBasisproof · cited by 5
- IsLocallyConstant.tfaeproof · cited by 5