sumElim — Mathlib

English

sumElim maps inl x to f x and inr y to g y; it is a finitely supported function on α ⊕ β with values in γ when f,g: α →₀ γ, β →₀ γ.

Русский

sumElim переводит inl x в f x и inr y в g y; это конечноподдерживаемая функция на α ⊕ β со значениями в γ.

LaTeX

$$$\text{sumElim} : (α \to_0 γ) \to (β \to_0 γ) \to (α \oplus β) \to_0 γ$$$

Lean4

/-- `Finsupp.sumElim f g` maps `inl x` to `f x` and `inr y` to `g y`. -/
@[simps support]
def sumElim {α β γ : Type*} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) : α ⊕ β →₀ γ
    where
  support := f.support.disjSum g.support
  toFun := Sum.elim f g
  mem_support_toFun := by simp

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