directSum_var — Mathlib

English

For the presentation of a direct sum, the coordinate corresponding to i is the image under lof of the i-th component of the i-th presentation.

Русский

Для презентации прямой суммы координата, соответствующая i-му, есть образ под lof от i-й компоненты презентации.

LaTeX

$$$(\\text{directSum pres}).var \\langle i,g\\rangle = \\operatorname{lof} A\\;\\iota\\;M\\;i\\;((pres(i)).var\\; g)$$$

Lean4

@[simp]
theorem directSum_var (pres : ∀ (i : ι), Presentation A (M i)) (i : ι) (g : (pres i).G) :
    (directSum pres).var ⟨i, g⟩ = lof A ι M i ((pres i).var g) :=
  rfl

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