directSum_var — Mathlib

English

In the direct sum solution, the i-th component of the solution is the corresponding i-th component projected into the i-th summand via lof.

Русский

В компоненте i решения прямой суммы соответствующая часть проецируется в i-ю слагаемую через lof.

LaTeX

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

Lean4

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

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