Skip Two Indices in Fin

This file provides the Fin.skipTwo function which maps Fin n to Fin (n+2) by skipping two specified indices.

Main definitions

• Fin.skipTwo i j hij - Given i < j in Fin (n+2), produces a function Fin n → Fin (n+2) that skips both i and j

Main results

• Fin.skipTwo_injective - skipTwo is injective
• Fin.skipTwo_strictMono - skipTwo is strictly monotone
• Fin.skipTwo_range - The range of skipTwo i j is exactly {i, j}ᶜ
• Fin.skipTwo_ne_first - skipTwo i j k ≠ i for all k
• Fin.skipTwo_ne_second - skipTwo i j k ≠ j for all k
• Fin.skipTwo_inverse - Every element not equal to i or j is in the range

Implementation notes

This module provides the canonical location for the Fin.skipTwo definition and its API lemmas. Files that need skipTwo functionality (such as DesnanotJacobi.lean) import this module and may define local abbreviations for convenience.

References

The skipTwo function is the natural generalization of Fin.succAbove (which skips one index) to skipping two indices. It arises in:

• Desnanot-Jacobi identity proofs (removing two rows/columns from a matrix)
• Pfaffian computations (perfect matching induction)
• Tiling decompositions (removing boundary elements)

def Fin.skipTwo {n : ℕ} (i j : Fin (n + 2)) (_hij : i < j) : Fin n → Fin (n + 2)

Remove two elements from Fin (n+2) to get Fin n. Given i < j in Fin (n+2), we map Fin n to Fin (n+2) by skipping i and j.

The function is defined piecewise:

• If k < i, then skipTwo i j k = k
• If i ≤ k and k + 1 < j, then skipTwo i j k = k + 1
• If k + 1 ≥ j, then skipTwo i j k = k + 2

Equations

• i.skipTwo j _hij k = if ↑k < ↑i then ⟨↑k, ⋯⟩ else if ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩

theorem Fin.skipTwo_injective {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) : Function.Injective (i.skipTwo j hij)

skipTwo is injective.

theorem Fin.skipTwo_strictMono {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) : StrictMono (i.skipTwo j hij)

skipTwo is strictly monotone.

theorem Fin.skipTwo_inverse {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) (x : Fin (n + 2)) (hx_ne_i : x ≠ i) (hx_ne_j : x ≠ j) : ∃ (k : Fin n), i.skipTwo j hij k = x

Every element not equal to i or j is in the range of skipTwo. This is the key lemma for constructing the inverse of skipTwo on its range.

theorem Fin.skipTwo_range {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) : Set.range (i.skipTwo j hij) = {x : Fin (n + 2) | x ≠ i ∧ x ≠ j}

The range of skipTwo is exactly the elements not equal to i or j.

theorem Fin.skipTwo_ne_first {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) (k : Fin n) : i.skipTwo j hij k ≠ i

skipTwo never returns its first skipped element.

theorem Fin.skipTwo_ne_second {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) (k : Fin n) : i.skipTwo j hij k ≠ j

skipTwo never returns its second skipped element.

theorem Fin.skipTwo_mem_compl {n : ℕ} (i j : Fin (n + 2)) (hij : i < j) (k : Fin n) : i.skipTwo j hij k ∈ {i, j}ᶜ

skipTwo gives values in the complement of {i, j}.