Theorems · Theorem · general topology
nhdsWithin_empty
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a ∅ = ⊥- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 52 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsproof · cited by 5,554
- Bot.botstatement and proof · cited by 4,720
- nhdsWithinstatement · cited by 1,912
- Filter.principal_emptyproof · cited by 19
- inf_bot_eqproof · cited by 14
Cited by16
Results whose statement or proof uses this declaration.
- leftLim_eq_of_isBotproof · cited by 5
- SuccOrder.nhdsGTproof · cited by 5
- eVariationOn.eVariationOn_on_inter_Iic_eq_Iio_add_edistproof · cited by 4
- PredOrder.nhdsLTproof · cited by 3
- MonotoneOn.tendsto_nhdsLTproof · cited by 3
- nhdsWithin_biUnionproof · cited by 2
- Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSetproof · cited by 2
- LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_leftproof · cited by 2
- map_coe_atTop_of_Ioo_subsetproof · cited by 2
- BoundedVariationOn.exists_tendsto_leftproof · cited by 2
- Convex.nhdsWithin_sdiff_eq_nhdsGTproof · cited by 2
- Convex.nhdsWithin_sdiff_eq_nhdsLTproof · cited by 2