measurable_apply — Mathlib

English

For any appropriate spaces, the evaluation map that sends (x, f) to f(x) is measurable.

Русский

Оценочное отображение, отправляющее (x, f) в f(x), измеримо.

LaTeX

$$MeasurableApply'(x) : Measurable (fun (x : E) (f : E →L[𝕜] F) => f x)$$

Lean4

@[fun_prop, measurability]
theorem measurable_apply [MeasurableSpace F] [BorelSpace F] (x : E) : Measurable fun f : E →L[𝕜] F => f x :=
  (apply 𝕜 F x).continuous.measurable

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