English
For any α and any list is of α, permutationsAux [] is the empty list. In other words, the auxiliary permutation generator yields no lists when the first argument is empty.
Русский
Для любого множества α и любого списка is из α, permutationsAux [] равно пустому списку. Иначе говоря, вспомогательный генератор перестановок не порождает списков, если первый аргумент пуст.
LaTeX
$$$$\text{permutationsAux }([]: List\ α)\ is = \ ([]) .$$$$
Lean4
@[simp]
theorem permutationsAux_nil (is : List α) : permutationsAux [] is = [] := by rw [permutationsAux, permutationsAux.rec]