perm_of_nodup_nodup_toFinset_eq — Mathlib

English

If l and l' are nodup and l.toFinset = l'.toFinset, then l ~ l'.

Русский

Если l и l' без повторов, и l.toFinset = l'.toFinset, тогда l ~ l'.

LaTeX

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

Lean4

theorem perm_of_nodup_nodup_toFinset_eq (hl : Nodup l) (hl' : Nodup l') (h : l.toFinset = l'.toFinset) : l ~ l' :=
  by
  rw [← Multiset.coe_eq_coe]
  exact Multiset.Nodup.toFinset_inj hl hl' h

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