pos_of_mem_ball

Mathlib.Analysis.Calculus.BumpFunction.Basic

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

English

The bump equals 1 eventually near c: f =ᶠ[𝓝 c] 1.

Русский

Вблизи центра c всплеск принимает значение 1 почти повсюду: f =ᶠ[𝓝 c] 1.

LaTeX

$$$ f =^\!_{{𝓝 c}} 1 $$$

Lean4

theorem pos_of_mem_ball (hx : x ∈ ball c f.rOut) : 0 < f x :=
  f.nonneg.lt_of_ne' <| by rwa [← support_eq, mem_support] at hx

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

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

Разделы

Аффилиация

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