memLp_zero

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.memLp_zero

English

Every simple function lies in L^0(μ).

Русский

Каждая простая функция принадлежит L^0(μ).

LaTeX

$$$f \\in L^0(\\mu)$$$

Lean4

theorem memLp_zero (f : α →ₛ E) (μ : Measure α) : MemLp f 0 μ :=
  memLp_zero_iff_aestronglyMeasurable.mpr f.aestronglyMeasurable

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

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

Разделы

Аффилиация

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