sumElim_apply

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.sumElim_apply

English

For f: α →₀ γ and g: β →₀ γ and x ∈ α ⊕ β, sumElim f g x equals Sum.elim f g x.

Русский

Для f: α →₀ γ, g: β →₀ γ и x ∈ α ⊕ β, sumElim f g x = Sum.elim f g x.

LaTeX

$$$\text{sumElim } f\; g\; x = \text{Sum.elim } f g x$$$

Lean4

theorem sumElim_apply {α β γ : Type*} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α ⊕ β) : sumElim f g x = Sum.elim f g x :=
  rfl

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

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

Разделы

Аффилиация

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