neg_smul_neg

Mathlib.MeasureTheory.Function.Holder

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

English

Negating the first and second Hp-space functions yields the same product as negating the result.

Русский

Отрицание в обе стороны даёт тот же результат в произведении.

LaTeX

$$−f • −g = f • g in Lp-sense.$$

Lean4

protected theorem neg_smul_neg (f : Lp 𝕜 p μ) (g : Lp E q μ) : -f • -g = f • g := by simp

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

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

Разделы

Аффилиация

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