English
For a decidable predicate of membership in s, mulIndicator f times mulIndicator g equals the piecewise combination of f and g on s and sᶜ.
Русский
При наличии разрешимого предиката принадлежности к s произведение индикаторов равно разбиению на случай: на s используется f, на sᶜ — g.
LaTeX
$$$$ \\text{with decidable } (x\\in s):\\quad s.mulIndicator f \\cdot s^c.mulIndicator g = s.piecewise(f,g) $$$$
Lean4
@[to_additive]
theorem mulIndicator_mul_compl_eq_piecewise [DecidablePred (· ∈ s)] (f g : α → M) :
s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g :=
by
ext x
by_cases h : x ∈ s
·
rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
·
rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
