range_toLp — Mathlib

English

Definition of toLp for ContinuousMap aligns with the standard Lp construction via a suitable isometry.

Русский

Определение toLp для ContinuousMap согласуется с обычной конструкцией Lp через изометрическое отображение.

LaTeX

$$$\\text{toLp is the composition of the isometric embedding with bounded continuous functions.}$$$

Lean4

theorem range_toLp :
    (LinearMap.range (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)).toAddSubgroup =
      MeasureTheory.Lp.boundedContinuousFunction E p μ :=
  by
  refine SetLike.ext' ?_
  have := (linearIsometryBoundedOfCompact α E 𝕜).surjective
  convert Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)
  rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup, LinearMap.coe_range]

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