eLpNorm_enorm — Mathlib

English

If f and g are almost everywhere equal, then MemLp f p μ is equivalent to MemLp g p μ.

Русский

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

LaTeX

$$$(f=g\text{ a.e.})\Rightarrow (MemLp\; f\; p\; μ \leftrightarrow MemLp\; g\; p\; μ).$$$

Lean4

@[simp]
theorem eLpNorm_enorm (f : α → ε) : eLpNorm (fun x ↦ ‖f x‖ₑ) p μ = eLpNorm f p μ :=
  eLpNorm_congr_enorm_ae <| Eventually.of_forall fun _ => enorm_enorm _

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