eLpNorm_mk_lt_top — Mathlib

English

An α-measurable function f belongs to Lp E p μ iff f ∈ MemLp f p μ.

Русский

Функция f принадлежит Lp E p μ тогда и только тогда, когда f ∈ MemLp f p μ.

LaTeX

$$f ∈ Lp E p μ ↔ MemLp f p μ$$

Lean4

theorem eLpNorm_mk_lt_top {α E : Type*} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {p : ℝ≥0∞}
    {f : α → E} (hfp : MemLp f p μ) : eLpNorm (AEEqFun.mk f hfp.1) p μ < ∞ := by simp [hfp.2]

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