English
Let s be a subset of α, r a function α → R, m an element of M, and a an element of α. Then the indicator of the function a ↦ r(a) · m on s equals the product of the indicator of r on a and m; i.e., (indicator s (r · • m)) a = (indicator s r a) · m for all a ∈ α.
Русский
Пусть s ⊆ α, r : α → R, m ∈ M и a ∈ α. Тогда индикатор функции a ↦ r(a) · m на множестве s равен произведению индикатора r на a и m; то есть (indicator s (r · • m)) a = (indicator s r a) · m для всех a ∈ α.
LaTeX
$$$\\\\forall s:\\\\mathcal{P}(\\\\alpha), \\\\forall r: \\\\alpha \to R, \\\\forall m: M, \\\\forall a: \\\\alpha, \\\\mathrm{indicator}_s (r \\\\cdot \\\\mathbf{•} m) (a) = \\\\mathrm{indicator}_s r (a) \\\\cdot m$$$
Lean4
theorem indicator_smul_const_apply (s : Set α) (r : α → R) (m : M) (a : α) :
indicator s (r · • m) a = indicator s r a • m :=
indicator_smul_apply_left _ _ _ _
