English
For a smooth bump function f, the support of f equals the intersection of the chart source with the preimage under extChartAt of the ball centered at extChartAt c c with radius f.rOut.
Русский
Для гладкой bump-функции f множество её опорного множества совпадает с пересечением области диаграммы и предобраза по extChartAt шара с центром в extChartAt c c и радиусом f.rOut.
LaTeX
$$$\operatorname{supp}(f) = (chartAt H c).source \cap (extChartAt I c)^{-1}(\mathrm{ball}(extChartAt I c c, f.rOut)).$$$
Lean4
theorem support_eq_inter_preimage :
support f = (chartAt H c).source ∩ extChartAt I c ⁻¹' ball (extChartAt I c c) f.rOut := by
rw [coe_def, support_indicator, support_comp_eq_preimage, ← extChartAt_source I, ←
(extChartAt I c).symm_image_target_inter_eq', ← (extChartAt I c).symm_image_target_inter_eq', f.support_eq]
