Theorems · Theorem · combinatorics

Fin.cons_snoc_eq_snoc_cons

∀ {n : ℕ} {β : Sort u_2} (a : β) (q : Fin n → β) (b : β), Fin.cons a (Fin.snoc q b) = Fin.snoc (Fin.cons a q) b

cons and snoc commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

3 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound