Theorems · Theorem · general topology
IsOpen.mem_nhds
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsOpen s → x ∈ s → s ∈ nhds x- Defined in
- Mathlib.Topology.Neighborhoods
- Cited by
- 470 results in Mathlib
- Foundations
- Depth 59 from the axioms, rests on 633 definitions · 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
- mem_nhds_iffproof · cited by 67
- Set.Subset.reflproof · cited by 66
Cited by470
Results whose statement or proof uses this declaration.
- continuous_iff_continuousAtproof · cited by 139
- Metric.ball_mem_nhdsproof · cited by 64
- TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_openproof · cited by 58
- gt_mem_nhdsproof · cited by 37
- Iio_mem_nhdsproof · cited by 34
- Ioi_mem_nhdsproof · cited by 27
- Ioo_mem_nhdsproof · cited by 27
- Metric.eball_mem_nhdsproof · cited by 25
- IsOpen.eventually_memproof · cited by 24
- nhds_discreteproof · cited by 23
- OpenPartialHomeomorph.continuousAtproof · cited by 23
- Topology.IsOpenEmbedding.map_nhds_eqproof · cited by 22
Showing the 200 most cited of 470.