inner — Mathlib

English

If f,g are measurable, then t ↦ ⟪f(t), g(t)⟫ is measurable.

Русский

Пусть f и g измеримы; тогда t ↦ ⟪f(t), g(t)⟫ измеримо.

LaTeX

$$$\\text{Measurable.inner}$$$

Lean4

@[aesop safe 20 apply (rule_sets := [Measurable]), fun_prop]
theorem inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
    {f g : α → E} (hf : Measurable f) (hg : Measurable g) : Measurable fun t => ⟪f t, g t⟫ :=
  Continuous.measurable2 continuous_inner hf hg

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