coeFn_toLp — Mathlib

English

If μ is an OpenPosMeasure, then the map toLp is injective on bounded continuous functions modulo μ-a.e. equality.

Русский

При μ OpenPosMeasure отображение toLp инъективно по отношению к эквивалентности μ-почти равенства.

LaTeX

$$$\\text{toLp is injective on } BoundedContinuousFunction \\text{ under } μ. $$$

Lean4

theorem coeFn_toLp (f : α →ᵇ E) : toLp (E := E) p μ 𝕜 f =ᵐ[μ] f :=
  AEEqFun.coeFn_mk f _

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