memLp_one_iff_integrable — Mathlib

English

For any function f, f belongs to L^1(μ) if and only if f is integrable with respect to μ.

Русский

Для любой функции f принадлежность к L^1(μ) эквивалентна интегрируемости по μ.

LaTeX

$$$\operatorname{MemLp}(f, 1, \mu) \iff \operatorname{Integrable}(f, \mu)$$$

Lean4

theorem memLp_one_iff_integrable {f : α → ε} : MemLp f 1 μ ↔ Integrable f μ := by
  simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]

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