toFinset_inj — Mathlib

English

If l and l' are nodup multisets and have the same toFinset, then l = l'.

Русский

Если два мультимножества без повторов имеют одинаковое toFinset, то они равны.

LaTeX

$$$\\forall l\\, l' : \\mathsf{Multiset}\\,\\alpha\\, (hl : l.Nodup) (hl' : l'.Nodup) (h : l.toFinset = l'.toFinset),\\; l = l'$$$

Lean4

theorem toFinset_inj {l l' : Multiset α} (hl : Nodup l) (hl' : Nodup l') (h : l.toFinset = l'.toFinset) : l = l' := by
  simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

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