ext_component — Mathlib

English

If two elements f and g of the direct sum have the same i-th components for every i, then f = g.

Русский

Если две манеры элементов прямой суммы f и g имеют одинаковые i-ые компоненты для каждого i, то f = g.

LaTeX

$$$\\forall f,g\\in\\bigoplus_{i} M_i,\\; (\\forall i,\\ \\mathrm{component}_i(f)=\\mathrm{component}_i(g))\\Rightarrow f=g.$$$

Lean4

theorem ext_component {f g : ⨁ i, M i} (h : ∀ i, component R ι M i f = component R ι M i g) : f = g :=
  DFinsupp.ext h

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