toLp_inj — Mathlib

English

Two continuous maps are equal if and only if their Lp images coincide under the open-positive measure hypothesis.

Русский

Две последовательные карты равны тогда и только тогда, когда их изображения в Lp совпадают при условии открытого положительного измерения.

LaTeX

$$HasSum equality equivalence: toLp(p, μ, 𝕜)f = toLp(p, μ, 𝕜)g ⇔ f = g$$

Lean4

theorem toLp_inj {f g : C(α, E)} [μ.IsOpenPosMeasure] : toLp (E := E) p μ 𝕜 f = toLp (E := E) p μ 𝕜 g ↔ f = g :=
  (toLp_injective μ).eq_iff

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