fst_sumFinsuppEquivProdFinsupp — Mathlib

English

For any f: α ⊕ β →₀ γ and x ∈ α, the first component of the sumFinsuppEquivProdFinsupp f equals f (Sum.inl x).

Русский

Для любого f: α ⊕ β →₀ γ первый компонент эквивалентности равен f(Sum.inl x).

LaTeX

$$$(\text{sumFinsuppEquivProdFinsupp } f).1");x = f(\text{Sum.inl } x)$$$

Lean4

theorem fst_sumFinsuppEquivProdFinsupp {α β γ : Type*} [Zero γ] (f : α ⊕ β →₀ γ) (x : α) :
    (sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x) :=
  rfl

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