sublists_perm_sublists' — Mathlib

English

For any list l of α, the two lists sublists l and sublists' l are permutations of one another.

Русский

Для любого списка l над α подсписки l и подсписки l' образуют одну и ту же последовательность в другом порядке; они равны по существующей перестановке.

LaTeX

$$$$ \\text{l.sublists} \\;\\sim\\; \\text{sublists'}\\,l $$$$

Lean4

theorem sublists_perm_sublists' (l : List α) : sublists l ~ sublists' l :=
  by
  rw [← finRange_map_get l, sublists_map, sublists'_map]
  apply Perm.map
  apply (perm_ext_iff_of_nodup _ _).mpr
  · simp
  · exact nodup_sublists.mpr (nodup_finRange _)
  · exact (nodup_sublists'.mpr (nodup_finRange _))

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