English
For any neighborhood-s, the neighborhood basis of c can be refined by supports of bump functions contained in s.
Русский
Для любого окрестности s в окрестности c существует база, состоящая из опор функций-амплитуд, вложенных в s.
LaTeX
$$$(\ nhds c).HasBasis (\lambda f : SmoothBumpFunction I c, tsupport f \subseteq s) (\lambda f, \operatorname{support}(f))$$
Lean4
/-- Given `s ∈ 𝓝 c`, the supports of smooth bump functions `f : SmoothBumpFunction I c` such that
`tsupport f ⊆ s` form a basis of `𝓝 c`. In other words, each of these supports is a
neighborhood of `c` and each neighborhood of `c` includes `support f` for some
`f : SmoothBumpFunction I c` such that `tsupport f ⊆ s`. -/
theorem nhds_basis_support {s : Set M} (hs : s ∈ 𝓝 c) :
(𝓝 c).HasBasis (fun f : SmoothBumpFunction I c => tsupport f ⊆ s) fun f => support f :=
((nhds_basis_tsupport c).restrict_subset hs).to_hasBasis' (fun f hf => ⟨f, hf.2, subset_closure⟩) fun f _ =>
f.support_mem_nhds
