toFinset_eq_iff_perm_dedup — Mathlib

English

For lists l, l', l.toFinset = l'.toFinset iff l.dedup ∼ l'.dedup.

Русский

Для списков l, l' равенство toFinset эквивалентно тому, что dedup(l) и dedup(l') являются перестановками.

LaTeX

$$$\\forall {l l' : \\mathsf{List}\\,\\alpha},\\; l.toFinset = l'.toFinset \\iff l.dedup \\sim l'.dedup$$$

Lean4

theorem toFinset_eq_iff_perm_dedup : l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup := by
  simp [Finset.ext_iff, perm_ext_iff_of_nodup (nodup_dedup _) (nodup_dedup _)]

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