English
Let α be a space with suitable topology and measure μ, and let E be a normed space. For every bounded continuous map f: α → E, the Lp representation obtained from the continuous-map realization agrees with the Lp representation obtained from the bounded-continuous realization; i.e. the two natural ways of viewing f inside Lp coincide.
Русский
Пусть пространство α имеет подходящую топологию, μ — меру, E — нормированное пространство. Для любой ограниченной непрерывной функции f: α → E представление в пространстве Lp, получаемое через отображение в непрерывную карту, совпадает с представлением через отображение ограниченно непрерывной функции; то есть два естественных способа рассмотреть f в Lp совпадают.
LaTeX
$$$toLp\left(E := E\right)\ p\ μ\ 𝕜\ f^{\text{toContinuousMap}} =\ BoundedContinuousFunction.toLp\left(E := E\right)\ p\ μ\ 𝕜\ f$$$
Lean4
@[simp]
theorem toLp_comp_toContinuousMap (f : α →ᵇ E) :
toLp (E := E) p μ 𝕜 f.toContinuousMap = BoundedContinuousFunction.toLp (E := E) p μ 𝕜 f :=
rfl
