inner_const — Mathlib

English

If f is measurable, then t ↦ ⟪f(t), c⟫ is measurable for any fixed c.

Русский

Пусть f измерима; тогда для фиксированного c, t ↦ ⟪f(t), c⟫ измеримо.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem inner_const {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
    {c : E} {f : α → E} (hf : Measurable f) : Measurable fun t => ⟪f t, c⟫ :=
  Measurable.inner hf measurable_const

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