Theorems · Theorem · order theory

Fin.succAbove_succAbove_succAbove_predAbove

∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n),
  (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Given i : Fin (n + 2) and j : Fin (n + 1), there are two ways to represent the order embedding Fin n → Fin (n + 2) leaving holes at i and i.succAbove j. One is i.succAbove ∘ j.succAbove. It corresponds to embedding Fin n to Fin (n + 1) leaving a hole at j, then embedding the result to Fin (n + 2) leaving a hole at i. The other one is (i.succAbove j).succAbove ∘ (j.predAbove i).succAbove. It corresponds to swapping the roles of i and j. This lemma says that these two ways are equal. It is used in Fin.removeNth_removeNth_eq_swap to show that two ways of removing 2 elements from a sequence give the same answer.

Defined in

Mathlib.Data.Fin.SuccPred

Cited by

1 results in Mathlib

Foundations

Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound