Theorems · Theorem · general topology
nhdsWithin_insert
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s : Set α), nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 64 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.
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 and proof · cited by 8,121
- nhdsWithinstatement and proof · cited by 1,912
- nhdsWithin_unionproof · cited by 41
- Set.singleton_unionproof · cited by 22
- nhdsWithin_singletonproof · cited by 12
Cited by13
Results whose statement or proof uses this declaration.
- contMDiffWithinAt_insert_selfproof · cited by 5
- Filter.EventuallyEq.iteratedFDerivWithin_eqproof · cited by 3
- mem_nhdsWithin_insertproof · cited by 3
- Asymptotics.isLittleOTVS_insertproof · cited by 2
- Asymptotics.isBigOWith_insertproof · cited by 2
- contDiffWithinAt_insert_selfproof · cited by 2
- Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insertproof · cited by 1
- PredOrder.nhdsLEproof · cited by 1
- insert_mem_nhdsWithin_insertproof · cited by 1
- contDiffWithinAt_iff_of_ne_inftyproof · cited by 1
- CovBy.nhdsGEproof · cited by 0
- CovBy.nhdsLEproof · cited by 0