getElem_cons_eraseIdx_perm — Mathlib

English

If h : n < length(l), then the list conjoining the nth element with the rest after eraseIdx n is a permutation of l.

Русский

Если h : n < длина(l), тогда элемент с индексом n, затем l.eraseIdx n переставляются в l.

LaTeX

$$$\\forall h:\\, n < |l|,\\; (l[n] :: l.eraseIdx n) \\sim l.$$$

Lean4

theorem getElem_cons_eraseIdx_perm {n : ℕ} (h : n < l.length) : l[n] :: l.eraseIdx n ~ l := by
  simpa [h] using (set_perm_cons_eraseIdx h l[n]).symm

Похожие утверждения