coe_smul — Mathlib

English

Compatibility of scalar action with coercion: the evaluation of c • m matches the action on the underlying function.

Русский

Согласование скалярного действия с редукцией: значение c • m совпадает с действием на базовой функции.

LaTeX

$$$\forall c:\, R,\forall m:\, OuterMeasure\ \alpha,\forall s:\, Set\ \alpha,\ (c \cdot m)\,s = c \cdot (m\,s).$$$

Lean4

@[simp]
theorem coe_smul (c : R) (m : OuterMeasure α) : ⇑(c • m) = c • ⇑m :=
  rfl

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