coe_piecewise — Mathlib

English

The coercion commutes with piecewise: the function obtained by coercion of x.piecewise y s equals the piecewise function of the coercions of x and y.

Русский

Коэрционность сохраняет операцию piecewise: отображение x.piecewise y s равняется piecewise, применённому к коэффициентам x и y.

LaTeX

$$$ \mathrm{coe}\bigl(x\text{.piecewise } y\, s\bigr) = s\text{.piecewise } (\mathrm{coe}\, x) (\mathrm{coe}\, y) $$$

Lean4

@[simp, norm_cast]
theorem coe_piecewise : ⇑(x.piecewise y s) = s.piecewise x y :=
  rfl

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