toList_cons — Mathlib

English

If a ∉ s, then (cons a s h).toList is permutation-equivalent to a :: s.toList.

Русский

Если a ∉ s, то toList (cons a s h) эквивалентен перестановке a :: s.toList.

LaTeX

$$$\\text{toList}((\\text{cons } a\\ s\\ h))\\;\\sim\\; a :: s.toList.$$$

Lean4

theorem toList_cons {a : α} {s : Finset α} (h : a ∉ s) : (cons a s h).toList ~ a :: s.toList :=
  (List.perm_ext_iff_of_nodup (nodup_toList _) (by simp [h, nodup_toList s])).2 fun x => by
    simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]

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