piecewise_eq_mulIndicator — Mathlib

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

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