range_toLpHom — Mathlib

English

The range of toLp equals the subgroup of Lp corresponding to bounded continuous functions; this is established via the surjectivity of the linear isometry given by compactness arguments.

Русский

Образ toLp совпадает с подгруппой Lp соответствующих ограниченных непрерывных функций; доказана через сюръективность линейного изометрирования.

LaTeX

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

Lean4

theorem range_toLpHom [Fact (1 ≤ p)] :
    ((toLpHom p μ).range : AddSubgroup (Lp E p μ)) = MeasureTheory.Lp.boundedContinuousFunction E p μ :=
  by
  symm
  exact
    AddMonoidHom.addSubgroupOf_range_eq_of_le ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E))
      (by rintro - ⟨f, rfl⟩; exact mem_Lp f : _ ≤ Lp E p μ)

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