lpTrimToLpMeas_ae_eq — Mathlib

English

Let hm be m ≤ m0 and f ∈ Lp F p (μ.trim hm). Then lpTrimToLpMeas F 𝕜 p μ hm f equals f μ-almost everywhere.

Русский

Пусть hm: m ≤ m0 и f ∈ Lp F p (μ.trim hm). Тогда lpTrimToLpMeas F 𝕜 p μ hm f равно f μ-непосредственно почти равны.

LaTeX

$$$lpTrimToLpMeas\ F\ 𝕜\ p\ μ\ hm\ f =_{\mu} f$$$

Lean4

theorem lpTrimToLpMeas_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) : lpTrimToLpMeas F 𝕜 p μ hm f =ᵐ[μ] f :=
  MemLp.coeFn_toLp (memLp_of_memLp_trim hm (Lp.memLp f))

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