toLpHom — Mathlib

English

The map toLp: bounded continuous functions to Lp is injective on the level of equivalence classes when μ is Open Pos Measure.

Русский

Отображение toLp инъективно на классах эквивалентности при мера μ OpenPosMeasure.

LaTeX

$$$\\text{toLp is injective under OpenPosMeasure: } f=g \\Rightarrow toLp(f)=toLp(g).$$$

Lean4

/-- The normed group homomorphism of considering a bounded continuous function on a finite-measure
space as an element of `Lp`. -/
def toLpHom [Fact (1 ≤ p)] : NormedAddGroupHom (α →ᵇ E) (Lp E p μ) :=
  { AddMonoidHom.codRestrict ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)) (Lp E p μ) mem_Lp with
    bound' := ⟨_, Lp_norm_le⟩ }

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