permutations_nil — Mathlib

English

The set of all permutations of the empty list is the singleton set containing the empty list itself: permutations([]) = [[]].

Русский

Множество всех перестановок пустого списка равно одиночному списку, содержащему пустой список: permutations([]) = [[]].

LaTeX

$$$$\text{permutations}([]) = [[]]$$$$

Lean4

@[simp]
theorem permutations_nil : permutations ([] : List α) = [[]] := by rw [permutations, permutationsAux_nil]

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