coe_def

Mathlib.Geometry.Manifold.BumpFunction

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

English

There is a CoeFun instance declaring SmoothBumpFunction as a function-valued object with canonical coercion to functions.

Русский

Существует инстанс коэффициентного отображения, объявляющий SmoothBumpFunction как функцию.

LaTeX

$$$\\text{SmoothBumpFunction.instCoeFunForallReal}$$$

Lean4

theorem coe_def : ⇑f = indicator (chartAt H c).source (f.toContDiffBump ∘ extChartAt I c) :=
  rfl

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

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

Разделы

Аффилиация

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