eq'

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

English

Integrable f μ is equivalent to f.FinMeasSupp μ (for ENNReal p).

Русский

Интегрируемость f эквивалентна FinMeasSupp f μ (для ENNReal p).

LaTeX

$$$\\mathrm{Integrable}(f,\\mu) \\iff f\\mathrm{.FinMeasSupp}(\\mu)$$$

Lean4

protected theorem eq' {f g : Lp.simpleFunc E p μ} : (f : α →ₘ[μ] E) = (g : α →ₘ[μ] E) → f = g :=
  Subtype.eq ∘ Subtype.eq

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

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

Разделы

Аффилиация

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