Theorems · Theorem · general topology
nhdsWithin_insert_of_ne
∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X} {s : Set X},
x ≠ y → nhdsWithin x (insert y s) = nhdsWithin x s- Defined in
- Mathlib.Topology.Separation.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceT1Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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
- LE.le.transproof · cited by 3,151
- IsOpenproof · cited by 2,400
- le_antisymmproof · cited by 2,068
- nhdsWithinstatement and proof · cited by 1,912
- T1Spacestatement and proof · cited by 275
- Set.Subset.rflproof · cited by 255
- Set.mem_singletonproof · cited by 183
- Set.sdiff_subsetproof · cited by 156
- Set.subset_insertproof · cited by 96
Cited by9
Results whose statement or proof uses this declaration.
- contDiffWithinAt_insertproof · cited by 4
- hasMFDerivWithinAt_insertproof · cited by 3
- continuousWithinAt_insertproof · cited by 3
- hasFDerivWithinAt_insertproof · cited by 2
- mdifferentiableWithinAt_insertproof · cited by 2
- HasFPowerSeriesWithinOnBall.hasFDerivWithinAtproof · cited by 1
- hasFPowerSeriesWithinAt_insertproof · cited by 0
- insert_mem_nhdsWithin_of_subset_insertproof · cited by 0
- HasFPowerSeriesWithinOnBall.differentiableOnproof · cited by 0