permutations' — Mathlib

English

The list of all permutations of the empty list equals the singleton list containing the empty list: permutations ([] : List α) = [[]].

Русский

Список всех перестановок пустого списка равен одноэлементному списку, состоящему из пустого списка: permutations ([] : List α) = [[]].

LaTeX

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

Lean4

theorem permutations' {s t : List α} (p : s ~ t) : permutations' s ~ permutations' t := by
  induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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