range_toLp — Mathlib

English

Equivalence of the range of the toLp map with the subgroup of bounded continuous Lp elements, as established by the previous lemmas.

Русский

Эквивалентность образа toLp и подгруппы ограниченных непрерывных элементов в Lp.

LaTeX

$$$\\mathrm{range}(\\mathrm{toLp}) = \\mathrm{Lp}_{\\text{bounded}}(E,p,μ).$$$

Lean4

theorem range_toLp :
    (LinearMap.range (toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)).toAddSubgroup =
      MeasureTheory.Lp.boundedContinuousFunction E p μ :=
  range_toLpHom p μ

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