toLp_zero

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

English

Under a finite measure μ, any simple function is integrable (variant).

Русский

При конечной мере μ любая простая функция интегрируема (вариант).

LaTeX

$$$[IsFiniteMeasure(\\mu)]\\Rightarrow \\mathrm{Integrable}(f,\\mu)$$$

Lean4

theorem toLp_zero : toLp (0 : α →ₛ E) MemLp.zero = (0 : Lp.simpleFunc E p μ) :=
  rfl

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

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

Разделы

Аффилиация

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