toLp_eq_mk

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

English

toLp respects subtraction: toLp(f-g) = toLp f - toLp g.

Русский

toLp сохраняет вычитание: toLp(f−g) = toLp f − toLp g.

LaTeX

$$$\\mathrm{toLp}(f-g, p, \\mu) = \\mathrm{toLp}(f,p,\\mu) - \\mathrm{toLp}(g,p,\\mu)$$$

Lean4

theorem toLp_eq_mk (f : α →ₛ E) (hf : MemLp f p μ) : (toLp f hf : α →ₘ[μ] E) = AEEqFun.mk f f.aestronglyMeasurable :=
  rfl

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

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

Разделы

Аффилиация

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