toLp_eq_toLp_iff — Mathlib

English

In the Lp space, the coeerce-to-Lp map sends a function represented by MemLp back to itself almost everywhere.

Русский

В пространстве Lp отображение приведения к Lp возвращает функцию, представленную MemLp, почти всюду.

LaTeX

$$hf.toLp f = f$$

Lean4

@[simp]
theorem toLp_eq_toLp_iff {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : hf.toLp f = hg.toLp g ↔ f =ᵐ[μ] g := by
  simp [toLp]

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