mulIndicator_symmDiff — Mathlib

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) _

Похожие утверждения