piecewise_compl — Mathlib

English

If s is complemented, then the piecewise with f,g is equal to the left-right swapped version on the complement: (s^c).piecewise f g = s.piecewise g f.

Русский

Для дополнения множества верна перестановка ветвей: (s^c).piecewise f g = s.piecewise g f.

LaTeX

$$$$\\bigl(s^{c}\\bigr).piecewise f g = s.piecewise g f.$$$$

Lean4

theorem piecewise_compl [DecidableEq ι] (s : Finset ι) [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ sᶜ)]
    (f g : ∀ i, π i) : sᶜ.piecewise f g = s.piecewise g f :=
  by
  ext i
  simp [piecewise]

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