memLp_congr_ae — Mathlib

English

If f and g are almost everywhere equal, then MemLp f p μ iff MemLp g p μ.

Русский

Если f и g равны почти всюду, то MemLp f p μ эквивалентно MemLp g p μ.

LaTeX

$$$\text{ae equality of } f,g \Rightarrow MemLp f p μ \Leftrightarrow MemLp g p μ.$$$

Lean4

theorem memLp_congr_ae [TopologicalSpace ε] {f g : α → ε} (hfg : f =ᵐ[μ] g) : MemLp f p μ ↔ MemLp g p μ := by
  simp only [MemLp, eLpNorm_congr_ae hfg, aestronglyMeasurable_congr hfg]

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