coeFn_neg

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.coeFn_neg

English

Negation commutes with almost everywhere equality in Lp: the function -f is ae-equal to -f.

Русский

Отрицание сохраняет почти всюду равенство в Lp: функция -f почти в эквивалентности равна -f.

LaTeX

$$(-f) =_{\mathrm{ae}} -f$$

Lean4

theorem coeFn_neg (f : Lp E p μ) : ⇑(-f) =ᵐ[μ] -f :=
  AEEqFun.coeFn_neg _

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

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

Разделы

Аффилиация

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