fun_const_smul — Mathlib

English

From a measurable two-argument smul, we obtain a measurable one-argument smul; i.e., a MeasurableSMul M X.

Русский

Измеримая двухарная операция SMul порождает измеримое однарное SMul.

LaTeX

$$$\text{MeasurableSMul } M X$ given $\text{MeasurableSMul_2 } M X$$$

Lean4

/-- Compositional version of `Measurable.const_smul` for use by `fun_prop`. -/
@[to_additive (attr := fun_prop) /-- Compositional version of `Measurable.const_vadd` for use by `fun_prop`. -/
    ]
theorem fun_const_smul {g : α → β → X} {h : α → β} (hg : Measurable ↿g) (hh : Measurable h) (c : M) :
    Measurable fun a ↦ (c • g a) (h a) :=
  (hg.comp <| measurable_id.prodMk hh).const_smul _

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