English
The map r sends a triple (i1,i2,i3) to the target index J by first composing i1 and i2 via π to obtain an intermediate index, then composing that with i3 again via π to land in J.
Русский
Отображение r переводит тройку индексов (i1,i2,i3) в целевой индекс J, сначала объединяя i1 и i2 с помощью π, а затем полученный результат объединяя с i3 через π.
LaTeX
$$$r:\\; I_1\\times I_2\\times I_3 \\to J\\; ,\\quad r(i_1,i_2,i_3)=\\pi\\_{{c_{12},c_3,c}}(\\langle \\pi\\_{c_1,c_2,c_{12}}\\langle i_1,i_2\\rangle , i_3\\rangle).$$$
Lean4
/-- The map `I₁ × I₂ × I₃ → j` that is obtained using `TotalComplexShape c₁ c₂ c₁₂`
and `TotalComplexShape c₁₂ c₃ c` when `c₁ : ComplexShape I₁`, `c₂ : ComplexShape I₂`,
`c₃ : ComplexShape I₃`, `c₁₂ : ComplexShape I₁₂` and `c : ComplexShape J`. -/
def r : I₁ × I₂ × I₃ → J := fun ⟨i₁, i₂, i₃⟩ ↦ π c₁₂ c₃ c ⟨π c₁ c₂ c₁₂ ⟨i₁, i₂⟩, i₃⟩
