piecewise_coe — Mathlib

English

Piecewise over a Finset corresponds to the piecewise over the corresponding Set when viewed as a set.

Русский

Piecewise над Finset соответствует piecewise над соответствующим множеством, когда Finset рассматривается как множество.

LaTeX

$$$(s : Set ι).\\text{piecewise } f g = s.\\text{piecewise } f g$$$

Lean4

@[norm_cast move]
theorem piecewise_coe [∀ j, Decidable (j ∈ (s : Set ι))] : (s : Set ι).piecewise f g = s.piecewise f g :=
  by
  ext
  congr

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