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