An auxiliary tri-partition of indices

This file contains a simple tri-partition of an index set that is used to form the triangular decompositions of both the Virasoro algebra and the Heisenberg algebra.

Main definitions

• indexTri: A partition of Option ℤ into three parts.

def VirasoroProject.indexTri (ε : SignType) : Set (Option ℤ)

The partition of Option ℤ into zero, positive, and negative parts.

Equations

• VirasoroProject.indexTri SignType.zero = {none, some 0}
• VirasoroProject.indexTri SignType.pos = some '' {n : ℤ | 0 < n}
• VirasoroProject.indexTri SignType.neg = some '' {n : ℤ | n < 0}

theorem VirasoroProject.pairwise_disjoint_indexTri : Pairwise fun (ε₁ ε₂ : SignType) => Disjoint (indexTri ε₁) (indexTri ε₂)

theorem VirasoroProject.iUnion_indexTri : ⋃ (ε : SignType), indexTri ε = Set.univ