sub

Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.sub

English

If f and g are MemLp, then f − g is MemLp with exponent p with respect to μ.

Русский

Если f и g принадлежат MemLp, то f − g принадлежит MemLp с той же экспонентой p по μ.

LaTeX

$$(hf : MemLp f p μ) → (hg : MemLp g p μ) → MemLp (f - g) p μ$$

Lean4

theorem sub {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f - g) p μ :=
  by
  rw [sub_eq_add_neg]
  exact hf.add hg.neg

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

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

Разделы

Аффилиация

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