English
The neighborhoods basis of c is given by tsupports of SmoothBumpFunctions.
Русский
Соседственные окрестности точки c задаются областию определения τtsupport гладких шляпочных функций.
LaTeX
$$$(\mathcal{N} c).HasBasis (\lambda f: SmoothBumpFunction I c, True) (\lambda f, \operatorname{tsupport}(f))$$$
Lean4
/-- The closures of supports of smooth bump functions centered at `c` form a basis of `𝓝 c`.
In other words, each of these closures is a neighborhood of `c` and each neighborhood of `c`
includes `tsupport f` for some `f : SmoothBumpFunction I c`. -/
theorem nhds_basis_tsupport : (𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f => tsupport f :=
by
have :
(𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
(extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) :=
by
rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c]
exact nhdsWithin_range_basis.map _
exact
this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) fun f _ => f.tsupport_mem_nhds
