indicator_smul — Mathlib

English

The value of the indicator of a scaled function at a point equals the scale factor times the indicator of the original function at that point.

Русский

Значение индикатора умноженной функции в точке равно коэффициенту умножения, умножающему исходную функцию в этой точке.

LaTeX

$$$ \mathrm{indicator}(s, (a \mapsto r(a) \cdot f(a))) = (a \mapsto r(a)) \cdot \mathrm{indicator}(s, f) $$$

Lean4

theorem indicator_smul (s : Set α) (r : α → R) (f : α → M) :
    indicator s (fun a ↦ r a • f a) = fun a ↦ r a • indicator s f a :=
  funext <| indicator_smul_apply s r f

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