English
For sets s and t, the indicator of the symmetric difference s Δ t satisfies mulIndicator (s Δ t) f = mulIndicator (s \\ t) f * mulIndicator (t \\ s) f.
Русский
Для множеств s и t индикатор симметричной разности удовлетворяет mulIndicator (s Δ t) f = mulIndicator (s \\ t) f * mulIndicator (t \\ s) f.
LaTeX
$$$\\mathrm{mulIndicator}(s \\Delta t) f = \\mathrm{mulIndicator}(s \\setminus t) f \\cdot \\mathrm{mulIndicator}(t \\setminus s) f$.$$
Lean4
@[to_additive]
theorem mulIndicator_symmDiff (s t : Set α) (f : α → M) :
mulIndicator (s ∆ t) f = mulIndicator (s \ t) f * mulIndicator (t \ s) f :=
mulIndicator_union_of_disjoint (disjoint_sdiff_self_right.mono_left sdiff_le) _