const_inner — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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