eq_one

Mathlib.Geometry.Manifold.BumpFunction

URI: https://scilib.ai/kg/mathlib#SmoothBumpFunction.eq_one

English

As above, the bump function attains the value 1 at the center c: f(c) = 1.

Русский

Как выше, bump-функция принимает значение 1 в точке центра: f(c) = 1.

LaTeX

$$$f(c) = 1.$$$

Lean4

@[simp]
theorem eq_one : f c = 1 :=
  f.eventuallyEq_one.eq_of_nhds

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

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

Разделы

Аффилиация

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