English
Let s be a subset of α, M a monoid with identity 1, and f: α → M. Then the function that equals f on s and 1 outside s coincides with the multiplicative indicator of s applied to f.
Русский
Пусть s ⊆ α, M — моноид с единицей 1, и f: α → M. Тогда функция, совпадающая с f на s и равная 1 вне s, равна умножающему индикатору по множеству s применённому к f.
LaTeX
$$$s\text{ piecewise } f\ 1 = s.mulIndicator f$$$
Lean4
@[to_additive (attr := simp)]
theorem piecewise_eq_mulIndicator [DecidablePred (· ∈ s)] : s.piecewise f 1 = s.mulIndicator f :=
funext fun _ => @if_congr _ _ _ _ (id _) _ _ _ _ Iff.rfl rfl rfl