getElem_permutations'Aux — Mathlib

English

The nth element of permutations'Aux x s equals s.insertIdx n x, provided n is within bounds.

Русский

n-й элемент permutations'Aux x s равен s.insertIdx n x при условии, что n в пределах диапазона.

LaTeX

$$$$ (permutations'Aux\ x\ s)[n] = s.insertIdx\ n\ x $$$$

Lean4

theorem getElem_permutations'Aux (s : List α) (x : α) (n : ℕ) (hn : n < length (permutations'Aux x s)) :
    (permutations'Aux x s)[n] = s.insertIdx n x := by
  induction s generalizing n with
  | nil =>
    simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn
    simp [hn]
  | cons y s IH =>
    cases n
    · simp
    · simpa [get] using IH _ _

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