length_permutations'Aux — Mathlib

English

For any list s and any element x, the length of permutations'Aux x s equals the length of s plus 1.

Русский

Для любого списка s и элемента x длина permutations'Aux x s равна длине s плюс 1.

LaTeX

$$$ \operatorname{length}(\operatorname{permutations'Aux} x s) = \operatorname{length}(s) + 1 $$$

Lean4

@[simp]
theorem length_permutations'Aux (s : List α) (x : α) : length (permutations'Aux x s) = length s + 1 := by
  induction s with
  | nil => simp
  | cons y s IH => simpa using IH

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