get_permutations'Aux — Mathlib

English

The nth element of permutations'Aux x s, when viewed as a list, equals s.insertIdx n x.

Русский

n-й элемент permutations'Aux x s равен s.insertIdx n x.

LaTeX

$$$$ (permutations'Aux\ x\ s).get\ ⟨n,\ hn⟩ = s.insertIdx\ n\ x $$$$

Lean4

theorem get_permutations'Aux (s : List α) (x : α) (n : ℕ) (hn : n < length (permutations'Aux x s)) :
    (permutations'Aux x s).get ⟨n, hn⟩ = s.insertIdx n x := by
  simp [getElem_permutations'Aux]
    -- Porting note: temporary theorem to solve diamond issue

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