smul_const — Mathlib

English

From a MeasurableSMul₂ M X, we obtain a MeasurableSMul M X; i.e., a canonical way to view a two-argument measurable action as a one-argument action.

Русский

Из MeasurableSMul₂ M X получаем MeasurableSMul M X; есть канонический переход двухарного измеримого действия к одномерному.

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem smul_const (hf : Measurable f) (y : X) : Measurable fun x => f x • y :=
  (MeasurableSMul.measurable_smul_const y).comp hf

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