toLp_injective — Mathlib

English

Under the hypothesis that μ is an open-positive measure, the map sending a bounded continuous map to its Lp representation is injective.

Русский

Пусть μ является открытым положительным измерением; отображение ограниченно непрерывной карты в её представление в Lp с сохранением норм является инъективным.

LaTeX

$$$\text{toLp}\left(p\ μ\ 𝕜 : C(α,E) \to Lp E p μ\right)\; \text{инъективно}$$$

Lean4

theorem toLp_injective [μ.IsOpenPosMeasure] : Function.Injective (⇑(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)) :=
  (BoundedContinuousFunction.toLp_injective _).comp (linearIsometryBoundedOfCompact α E 𝕜).injective

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