English
Let c1, c2, c3 be ComplexShape data and suppose total complex shapes give a coherent associativity among c1, c2, c3. Then the sign ε₂ satisfies the associativity-compatible equation: the ε₂ for the triple (c1₂, c3, c) applied to the composition π(c1,c2,c1₂)(i1,i2) and i3 equals the product of ε₂ for (c1, c2₃, c) applied to i1 and π(c2,c3,c2₃)(i2,i3) with ε₂(c2,c3,c2₃)(i2,i3) on the right.
Русский
Пусть даны тройки комплексных структур c1, c2, c3 и их совместные total-структуры образуют ассоциативную композицию. Тогда знаки ε₂ удовлетворяют тождеству совместимости с ассоциацией: ε₂(c₁₂,c₃,c)(π(c₁,c₂,c₁₂)(i₁,i₂), i₃) = ε₂(c₁,c₂₃,c)(i₁, π(c₂,c₃,c₂₃)(i₂,i₃)) · ε₂(c₂,c₃,c₂₃)(i₂,i₃).
LaTeX
$$$\\varepsilon_2(c_{12},c_3,c)(\\pi(c_1,c_2,c_{12})(i_1,i_2), i_3) =\\ \\varepsilon_2(c_1,c_2,c_{23})(i_1, \\pi(c_2,c_3,c_{23})(i_2,i_3)) \\cdot \\varepsilon_2(c_2,c_3,c_{23})(i_2,i_3).$$$
Lean4
theorem associative_ε₂_eq_mul (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
ε₂ c₁₂ c₃ c (π c₁ c₂ c₁₂ (i₁, i₂), i₃) = (ε₂ c₁ c₂₃ c (i₁, π c₂ c₃ c₂₃ (i₂, i₃)) * ε₂ c₂ c₃ c₂₃ (i₂, i₃)) := by
apply Associative.ε₂_eq_mul
