coe_sumElim — Mathlib

English

The coercion of sumElim f g equals the standard sumElim on functions: coe(sumElim f g) = Sum.elim (coe f) (coe g).

Русский

Указание коэрцирования sumElim совпадает с обычной операцией Sum.elim на функциях: coe(sumElim f g) = Sum.elim (coe f) (coe g).

LaTeX

$$$\\operatorname{coe}(\\text{sumElim } f\; g) = \\text{Sum.elim} (\\operatorname{coe} f) (\\operatorname{coe} g)$$$

Lean4

@[simp, norm_cast]
theorem coe_sumElim {α β γ : Type*} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) : ⇑(sumElim f g) = Sum.elim f g :=
  rfl

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