inner_const — Mathlib

English

If f: α → E is almost everywhere μ-measurable, then x ↦ ⟪f(x), c⟫ is almost everywhere μ-measurable for any fixed c ∈ E.

Русский

Пусть f: α → E является измеримой почти всюду по μ. Тогда x ↦ ⟪f(x), c⟫ измерима почти всюду по μ для любого фиксированного вектора c ∈ E.

LaTeX

$$$ (AEMeasurable\\ f\\ μ) \\rightarrow AEMeasurable\\ (\\lambda x, ⟪f(x), c⟫)\\ μ $$$

Lean4

@[measurability, fun_prop]
theorem inner_const {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
    {μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) : AEMeasurable (fun x => ⟪f x, c⟫) μ :=
  AEMeasurable.inner hf aemeasurable_const

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