English
An alternative expression of a neighborhood basis for nhdsWithin at range I using the images of extChartAt.
Русский
Альтернативное выражение базиса окрестностей nhdsWithin на range I через изображения extChartAt.
LaTeX
$$$(nhdsWithin (extChartAt I c).toFun c).HasBasis (fun _ => True) (fun f => \mathrm{image}(extChartAt I c)^{-1} (\cdot)).$$$
Lean4
/-- Given a smooth bump function `f : SmoothBumpFunction I c`, the closed ball of radius `f.R` is
known to include the support of `f`. These closed balls (in the model normed space `E`) intersected
with `Set.range I` form a basis of `𝓝[range I] (extChartAt I c c)`. -/
theorem nhdsWithin_range_basis :
(𝓝[range I] extChartAt I c c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
closedBall (extChartAt I c c) f.rOut ∩ range I :=
by
refine
((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_
?_
· rintro R ⟨hR0, hsub⟩
exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩
· exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos) self_mem_nhdsWithin
