measurable_coe — Mathlib

English

Let E and F be normed spaces over 𝕜, and consider the space of continuous linear maps L(E, F). The map Ev: L(E, F) × E → F given by Ev(T, x) = T(x) is measurable. In particular, for a fixed x ∈ E, the map T ↦ T(x) is measurable.

Русский

Пусть E и F — нормированные пространства над 𝕜, и возьмём пространство непрерывно линейных отображений L(E, F). Отображение Ev: L(E, F) × E → F, Ev(T, x) = T(x), измеримо. В частности, для фиксированного x ∈ E отображение T ↦ T(x) измеримо.

LaTeX

$$$\\operatorname{ev}:\\left(E \\to_L[𝕜] F\\right) \\times E \\to F,\\quad \\operatorname{ev}(T,x)=T(x) \\quad$ является измеримым.$$

Lean4

@[measurability]
theorem measurable_coe [MeasurableSpace F] [BorelSpace F] : Measurable fun (f : E →L[𝕜] F) (x : E) => f x :=
  measurable_pi_lambda _ measurable_apply

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