English
Let I1, I2, I12 be index types with TotalComplexShape c1, c2, c12. The map π on indices is the natural projection from I1 × I2 to I12 given by the total complex shape, i.e., π(i1, i2) = TotalComplexShape.π c1 c2 c12 (i1, i2).
Русский
Пусть I1, I2, I12 — множества индексов с Общей Формой Комплекса. Отображение π на индексах является естественной проекцией из I1 × I2 в I12, задаваемой через общую форму комплекса: π(i1, i2) = TotalComplexShape.π c1 c2 c12 (i1, i2).
LaTeX
$$$π : I_1 \times I_2 \to I_{12} \quad\text{with} \quad π(i_1,i_2) = TotalComplexShape.π c_1 c_2 c_{12} (i_1,i_2)$$$
Lean4
/-- The map `I₁ × I₂ → I₁₂` on indices given by `TotalComplexShape c₁ c₂ c₁₂`. -/
abbrev π (i : I₁ × I₂) : I₁₂ :=
TotalComplexShape.π c₁ c₂ c₁₂ i
