permutationsAux_nil — Mathlib

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]

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