mem_Lp_iff_memLp — Mathlib

English

Same as toLp_coeFn: a MemLp representative recovers the original function up to μ-almost everywhere equality.

Русский

То же, что и toLp_coeFn: представитель MemLp восстанавливает исходную функцию почти везде по μ.

LaTeX

$$(hf : MemLp f p μ) → hf.toLp f = f$$

Lean4

theorem mem_Lp_iff_memLp {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ MemLp f p μ := by
  simp [mem_Lp_iff_eLpNorm_lt_top, MemLp, f.stronglyMeasurable.aestronglyMeasurable]

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