apply_continuousLinearMap — Mathlib

English

Let φ: α → F →L[𝕜] E be a function measurable almost everywhere with respect to μ. Then for every v ∈ F, the map a ↦ φ(a)(v) is AEMeasurable (μ-almost everywhere measurable).

Русский

Пусть φ: α → F →L[𝕜] E измеримо почти всюду по μ. Тогда для каждого v ∈ F отображение a ↦ φ(a)(v) измеримо до почти-everywhere по μ.

LaTeX

$$$\\text{AEMeasurable}(\\phi, μ) \\Rightarrow \\forall v \\in F,\\ \\text{AEMeasurable}(a \\mapsto \\phi(a)(v), μ).$$$

Lean4

@[measurability]
theorem apply_continuousLinearMap {φ : α → F →L[𝕜] E} {μ : Measure α} (hφ : AEMeasurable φ μ) (v : F) :
    AEMeasurable (fun a => φ a v) μ :=
  (ContinuousLinearMap.apply 𝕜 E v).measurable.comp_aemeasurable hφ

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