toLp_def — Mathlib

English

For a continuous map f, the toLp definition coincides with the restriction to Lp of the linear isometry applied to f.

Русский

Для непрерывной карты f определение toLp совпадает с ограничением линейного изометрия на f.

LaTeX

$$$\\mathrm{toLp}(f) = \\mathrm{BoundedContinuousFunction.toLp}(f)$ как отображение.$$

Lean4

theorem toLp_def (f : C(α, E)) :
    toLp (E := E) p μ 𝕜 f = BoundedContinuousFunction.toLp (E := E) p μ 𝕜 (linearIsometryBoundedOfCompact α E 𝕜 f) :=
  rfl

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