elim_natCast_natCast

Mathlib.Data.Nat.Cast.Basic

URI: https://scilib.ai/kg/mathlib#Sum.elim_natCast_natCast

English

For α, β, γ with NatCast γ, and any n ∈ ℕ, Sum.elim (n : α → γ) (n : β → γ) = n.

Русский

Для любых α, β, γ с NatCast γ и любого n ∈ ℕ, Sum.elim (n) (n) = n.

LaTeX

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

Lean4

theorem elim_natCast_natCast {α β γ : Type*} [NatCast γ] (n : ℕ) : Sum.elim (n : α → γ) (n : β → γ) = n :=
  Sum.elim_lam_const_lam_const (γ := γ) n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru