normed_neg

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

English

If f is a ContDiffBump with center at 0 in E, then for every x, (f.normed μ)(-x) = (f.normed μ)(x).

Русский

Пусть f — ContDiffBump с центром в нуле. Тогда для всех x выполняется (f.normed μ)(-x) = (f.normed μ)(x).

LaTeX

$$$ f.normed \mu (-x) = f.normed \mu (x) $$$

Lean4

theorem normed_neg (f : ContDiffBump (0 : E)) (x : E) : f.normed μ (-x) = f.normed μ x := by
  simp_rw [f.normed_def, f.neg]

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

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

Разделы

Аффилиация

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