measurable_apply₂ — Mathlib

English

The map that sends (L, x) to L(x) is measurable, i.e., evaluation is measurable.

Русский

Отображение, которое отправляет (L, x) в L(x), измеримо.

LaTeX

$$$$\text{Measurable} \;\;\Big( (L,x) \mapsto L(x) \Big).$$$$

Lean4

theorem measurable_apply₂ [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither (E →L[𝕜] F) E]
    [MeasurableSpace F] [BorelSpace F] : Measurable fun p : (E →L[𝕜] F) × E => p.1 p.2 :=
  isBoundedBilinearMap_apply.continuous.measurable

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