zero_of_le_dist

Mathlib.Analysis.Calculus.BumpFunction.Basic

URI: https://scilib.ai/kg/mathlib#ContDiffBump.zero_of_le_dist

English

If dist(x, c) ≥ f.rOut then f(x) = 0; outside the outer ball, the bump vanishes.

Русский

Если расстояние dist(x, c) не меньше f.rOut, то f(x) = 0; вне внешнего шара всплеск обнуляется.

LaTeX

$$$ f.rOut \le \operatorname{dist}(x, c) \Rightarrow f(x)=0. $$$

Lean4

theorem zero_of_le_dist (hx : f.rOut ≤ dist x c) : f x = 0 := by rwa [← notMem_support, support_eq, mem_ball, not_lt]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru