Theorems · Definition · general topology
nhdsSetWithin
{X : Type u_1} → [TopologicalSpace X] → Set X → Set X → Filter XThe "neighbourhood within" filter for sets. Elements of 𝓝[t] s are sets containing the
intersection of t and a neighbourhood of s.
- Defined in
- Mathlib.Topology.Defs.Filter
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Filter.principalproof · cited by 740
- nhdsSetproof · cited by 267
Cited by25
Results whose statement or proof uses this declaration.
- IsCompact.nhdsSetWithin_prod_eqstatement · cited by 3
- nhdsSetWithin_selfstatement · cited by 2
- nhdsSetWithin_univstatement · cited by 2
- ContinuousOn.preimage_mem_nhdsSetWithinstatement and proof · cited by 2
- map_nhdsSet_induced_eqstatement and proof · cited by 1
- map_nhdsSet_subtype_valstatement and proof · cited by 1
- Topology.IsInducing.map_nhdsSet_eqstatement · cited by 1
- nhdsSetWithin_basis_openstatement · cited by 1
- Continuous.preimage_mem_nhdsSetWithinstatement and proof · cited by 1
- mem_nhdsSetWithinstatement and proof · cited by 1
- nhdsSetWithin_hasBasisstatement · cited by 1
- nhdsSetWithin_singletonstatement · cited by 0