inner — Mathlib

English

Let f,g: α → E be almost everywhere μ-measurable. Then the map x ↦ ⟪f(x), g(x)⟫ is almost everywhere μ-measurable.

Русский

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

LaTeX

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

Lean4

@[aesop safe 20 apply (rule_sets := [Measurable]), fun_prop]
theorem inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
    {μ : MeasureTheory.Measure α} {f g : α → E} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun x => ⟪f x, g x⟫) μ := by fun_prop

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