const_inner — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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