aefinStronglyMeasurable — Mathlib

English

For hf : MemLp f p μ with p ≠ 0 and p ≠ ∞, AEFinStronglyMeasurable f μ holds.

Русский

Пусть hf: MemLp f p μ с p ≠ 0 и p ≠ ∞; тогда выполняется AEFinStronglyMeasurable f μ.

LaTeX

$$$\text{MemLp}(f,p,\mu) \land p \neq 0 \land p \neq \infty \Longrightarrow \text{AEFinStronglyMeasurable}(f,\mu)$$$

Lean4

theorem aefinStronglyMeasurable (hf : Integrable f μ) : AEFinStronglyMeasurable f μ :=
  (memLp_one_iff_integrable.mpr hf).aefinStronglyMeasurable one_ne_zero ENNReal.coe_ne_top

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