English
If s ⊆ t, then mulIndicator (t \\ s) f = mulIndicator t f · (mulIndicator s f)⁻¹. The indicator on the set difference is the quotient of indicators.
Русский
Если s ⊆ t, то индикатор разности t\\s равен частному индикаторов t и s.
LaTeX
$$$$ \\forall s,t:\\ Set\\alpha, s\\subseteq t \\Rightarrow mulIndicator(t\\setminus s) f = mulIndicator t f · (mulIndicator s f)^{-1} $$$$
Lean4
@[to_additive indicator_diff']
theorem mulIndicator_diff (h : s ⊆ t) (f : α → G) : mulIndicator (t \ s) f = mulIndicator t f * (mulIndicator s f)⁻¹ :=
eq_mul_inv_of_mul_eq <|
by
rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self, union_eq_self_of_subset_right h]
exact disjoint_sdiff_self_left
