ext_component_iff — Mathlib

English

Two elements f and g in the direct sum are equal if and only if all their components are equal.

Русский

Два элемента прямой суммы равны тогда и только тогда, когда все их компоненты равны.

LaTeX

$$$f=g \\iff \\forall i, \\ \\mathrm{component}_i(f)=\\mathrm{component}_i(g).$$$

Lean4

theorem ext_component_iff {f g : ⨁ i, M i} : f = g ↔ ∀ i, component R ι M i f = component R ι M i g :=
  ⟨fun h _ ↦ by rw [h], ext_component R⟩

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