elim_intCast_intCast — Mathlib

English

For any α, β, γ, and [IntCast γ], the map Sum.elim n.cast n.cast equals n.cast: the piecewise constant casting agrees with the overall cast.

Русский

Для любых α, β, γ и [IntCast γ], Sum.elim n.cast n.cast = n.cast: разбиение по сумме согласуется с общим кастом.

LaTeX

$$$\\text{Sum.elim }(n.cast)\,(n.cast)=n.cast$$$

Lean4

@[simp]
theorem elim_intCast_intCast {α β γ : Type*} [IntCast γ] (n : ℤ) : Sum.elim (n : α → γ) (n : β → γ) = n :=
  Sum.elim_lam_const_lam_const (γ := γ) n

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