English
For any α, M with MulOneClass, and sets s,t ⊆ α with a function f: α → M, the equality mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a holds for all a.
Русский
Для любых α, M с MulOneClass и подмножеств s,t ⊆ α и функции f: α → M верно равенство mulIndicator (s ∪ t) f a · mulIndicator (s ∩ t) f a = mulIndicator s f a · mulIndicator t f a для всех a.
LaTeX
$$$\\mathrm{mulIndicator}(s \\cup t)\\, f\\, a \\;\\cdot\\; \\mathrm{mulIndicator}(s \\cap t)\\, f\\, a \;=\; \\mathrm{mulIndicator}(s)\\, f\\, a \\cdot \\mathrm{mulIndicator}(t)\\, f\\, a.$$$
Lean4
@[to_additive]
theorem mulIndicator_union_mul_inter (f : α → M) (s t : Set α) :
mulIndicator (s ∪ t) f * mulIndicator (s ∩ t) f = mulIndicator s f * mulIndicator t f :=
funext <| mulIndicator_union_mul_inter_apply f s t
