σ_ε₂ — Mathlib

English

For i1 and i2,i2' with c2.Rel i2 i2', the relation between σ and ε₂ expresses a compatibility: σ(i1,i2)·ε₂(i1,i2) equals ε₁(i2,i1)·σ(i1,i2').

Русский

Для i1 и пары i2,i2' удовлетворяющих relation c2, σ и ε₂ совместимы: σ(i1,i2)·ε₂(i1,i2) = ε₁(i2,i1)·σ(i1,i2').

LaTeX

$$$\\sigma c_1 c_2 c_{12} i_1 i_2 \\; \\varepsilon_2 c_1 c_2 c_{12} { fst := i_1, snd := i_2 } = \\varepsilon_1 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₂ i₂' : I₂} (h₂ : c₂.Rel i₂ i₂') :
    σ c₁ c₂ c₁₂ i₁ i₂ * ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ε₁ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ c₁ c₂ c₁₂ i₁ i₂' :=
  TotalComplexShapeSymmetry.σ_ε₂ i₁ h₂

Похожие утверждения