English
Let s be a subset of α and f, g: α → M with M a MulOneClass. Then for every a ∈ α, mulIndicator s (f(a) · g(a)) = mulIndicator s f(a) · mulIndicator s g(a). In other words, the multiplicative indicator distributes over pointwise multiplication.
Русский
Пусть s ⊆ α и f, g : α → M, где M — моноид с нейтральным элементом. Тогда для каждого a ∈ α выполняется: mulIndicator s (f(a) · g(a)) = mulIndicator s f(a) · mulIndicator s g(a). Другими словами, индикатор, умножаемый на произведение функций, равен произведению индикаторов.
LaTeX
$$$$ \\forall s \\subseteq \\alpha, \\forall f,g:\\alpha \\to M,\\quad \\mathrm{mulIndicator}(s)(f\\cdot g) = \\mathrm{mulIndicator}(s)f \\cdot \\mathrm{mulIndicator}(s)g $$$$
Lean4
@[to_additive]
theorem mulIndicator_mul' (s : Set α) (f g : α → M) : mulIndicator s (f * g) = mulIndicator s f * mulIndicator s g :=
mulIndicator_mul s f g
