toFinset_eq — Mathlib

English

Let s be a multiset with no duplicates (Nodup). Then the Finset obtained by Finset.mk s n with a proof n of Nodup is equal to s.toFinset.

Русский

Пусть s — мультимножество без повторов. Тогда конечное множество, получаемое как Finset.mk s n (с доказательством того, что s без повторов), равно s.toFinset.

LaTeX

$$$\\forall s : \\mathsf{Multiset}\\,\\alpha\\ (n : s.Nodup),\\; \\mathrm{Finset.mk}\\ s\\ n = s.toFinset$$$

Lean4

theorem toFinset_eq {s : Multiset α} (n : Nodup s) : Finset.mk s n = s.toFinset :=
  Finset.val_inj.1 n.dedup.symm

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