tsupport_eq

Mathlib.Analysis.Calculus.BumpFunction.Basic

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

English

Canonical coercion to functions is in place.

Русский

Имеется каноническое преобразование к функциям.

LaTeX

$$$ \text{CoeFun}_{\mathbb{R}}(ContDiffBump(c), E \to \mathbb{R}). $$$

Lean4

theorem tsupport_eq : tsupport f = closedBall c f.rOut := by
  simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']

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

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

Разделы

Аффилиация

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