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