ε — Mathlib · SciLib

English

A variant of the ε₂,ε₁ relation expresses the same anticommutation in terms of explicitly chosen indices, reflecting how horizontal and vertical signs interact.

Русский

Вариант тождества ε₂,ε₁ отражает то же самое anticommute-отношение для конкретных индексных выборок, иллюстрируя взаимодействие горизонтальных и вертикальных знаков.

LaTeX

$$$\\forall {i_1,i_1' : I_1} {i_2,i_2' : I_2}\\; c_1.Rel(i_1,i_1') \\Rightarrow\\; c_{12}.Rel(\\pi(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle),\\pi(c_1,c_2,c_{12})(\\langle i_1',i_2\\rangle))$$$

Lean4

/-- The signs which appear in the vertical differential of the total complex. -/
abbrev ε (i : I) : ℤˣ :=
  TensorSigns.ε' c i

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