English
For any i1,i1' related by c1 and i2, the relation between σ and ε₁,ε₂ expresses a compatibility: σ c1 c2 c12 i1 i2 times ε₁(...)(i1,i2) equals ε₂(...)(i2,i1) times σ(...)(i1',i2).
Русский
Для любых сопряжённых i1, i1' и i2 отображение σ совместимо с ε₁ и ε₂: σ(...,i1,i2)·ε₁(...) = ε₂(...)(i2,i1)·σ(...)(i1',i2).
LaTeX
$$$\\sigma c_1 c_2 c_{12} i_1 i_2 \\;\\varepsilon_1 c_1 c_2 c_{12} { fst := i_1, snd := i_2 } = \\varepsilon_2 c_2 c_1 c_{12} { fst := i_2, snd := i_1 } \\; \\sigma c_1 c_2 c_{12} i_1' i_2.$$$
Lean4
theorem σ_ε₁ {i₁ i₁' : I₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : I₂) :
σ c₁ c₂ c₁₂ i₁ i₂ * ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ε₂ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ c₁ c₂ c₁₂ i₁' i₂ :=
TotalComplexShapeSymmetry.σ_ε₁ h₁ i₂
