sum_univ_of — Mathlib

English

The map mk β s is injective; distinct coordinate data yield distinct elements of the direct sum.

Русский

Карта mk β s инъективна; различные данные координат дают различные элементы прямой суммы.

LaTeX

$$Injective (DirectSum.mk β s).$$

Lean4

theorem sum_univ_of [Fintype ι] (x : ⨁ i, β i) : ∑ i ∈ Finset.univ, of β i (x i) = x :=
  by
  apply DFinsupp.ext (fun i ↦ ?_)
  rw [DFinsupp.finset_sum_apply]
  simp [of_apply]

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