structure Finset.CombiDegen {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] (φ ψ : List ((i : ι) → α i)) : Type (max u_1 u_2)

• u (i : ι) : α i → ℤ
• sum_eq_zero (x : (i : ι) → α i) : x ∈ φ → ∑ i : ι, self.u i (x i) = 0
• sum_pos (x : (i : ι) → α i) : x ∈ ψ → 0 < ∑ i : ι, self.u i (x i)

def Finset.F3.φ : List (Fin 3 → Fin 9)

Equations

• Finset.F3.φ = [![0, 0, 0], ![1, 1, 1], ![2, 2, 2], ![3, 3, 3], ![4, 4, 4], ![7, 7, 7], ![8, 8, 8]]

def Finset.F3.ψ : List (Fin 3 → Fin 9)

Equations

• One or more equations did not get rendered due to their size.

def Finset.F3.u : Fin 3 → Fin 9 → ℤ

Equations

• Finset.F3.u = ![![-5, -5, -5, -5, -3, -1, -1, -3, -5], ![1, 4, 1, 5, 2, 5, 5, 2, 5], ![4, 1, 4, 0, 1, 5, 5, 1, 0]]

def Finset.F3.combiDegen : CombiDegen φ ψ

Equations

• Finset.F3.combiDegen = { u := Finset.F3.u, sum_eq_zero := Finset.F3.combiDegen._proof_1✝, sum_pos := Finset.F3.combiDegen._proof_2✝ }

def Finset.F2.φ : List (Fin 3 → Fin 2 → Fin 4)

Equations

• One or more equations did not get rendered due to their size.

def Finset.F2.ψ : List (Fin 3 → Fin 2 → Fin 4)

Equations

• One or more equations did not get rendered due to their size.

def Finset.F2.index (x : Fin 2 → Fin 4) : Fin 16

Equations

• Finset.F2.index x = ⟨4 * ↑(x 0) + ↑(x 1), ⋯⟩

def Finset.F2.u : Fin 3 → Fin 16 → ℤ

Equations

• One or more equations did not get rendered due to their size.

def Finset.F2.combiDegen : CombiDegen φ ψ

Equations

• Finset.F2.combiDegen = { u := fun (i : Fin 3) => Finset.F2.u i ∘ Finset.F2.index, sum_eq_zero := Finset.F2.combiDegen._proof_1✝, sum_pos := Finset.F2.combiDegen._proof_2✝ }