normed_sub — Mathlib

English

Let E be a normed space, μ a measure on E, and f a ContDiffBump centered at c. Then the normed bump is symmetric about c; for every x, (f.normed μ)(c − x) = (f.normed μ)(c + x).

Русский

Пусть E — нормированное пространство, μ — мера на E, и f — ContDiffBump с центром в c. Тогда нормированная бу́мпа симметрична относительно c: для каждого x выполняется (f.normed μ)(c − x) = (f.normed μ)(c + x).

LaTeX

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

Lean4

theorem normed_sub (x : E) : f.normed μ (c - x) = f.normed μ (c + x) := by simp_rw [f.normed_def, f.sub]

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