English
Let f be a smooth bump function centered at c in a manifold M, defined relative to a model I. If a point x lies in the source of the chart at c and the distance between extChartAt I c x and extChartAt I c c is at most rIn, then f(x) = 1.
Русский
Пусть f — гладкая функция-бамп, центрированная в точке c на многообразии M, заданная относительно модели I. Если точка x принадлежит области определения диаграммы в точке c и расстояние между extChartAt I c x и extChartAt I c c не превышает rIn, то f(x) = 1.
LaTeX
$$$\forall E [NormedAddCommGroup E] [NormedSpace \mathbb{R} E] \; {H} [TopologicalSpace H] \, {I : ModelWithCorners \mathbb{R} E H} \, {M} [TopologicalSpace M] \, [ChartedSpace H M] \, {c : M} \, (f : SmoothBumpFunction I c) \, {x : M},
\ x \in (chartAt H c).source \land dist (extChartAt I c x) (extChartAt I c c) \le f.rIn \Rightarrow f x = 1.$$
Lean4
theorem one_of_dist_le (hs : x ∈ (chartAt H c).source) (hd : dist (extChartAt I c x) (extChartAt I c c) ≤ f.rIn) :
f x = 1 := by simp only [f.eqOn_source hs, (· ∘ ·), f.one_of_mem_closedBall hd]
