toFinset_eq — Mathlib

English

If a nodup list l is given, then the Finset corresponding to l by toFinset equals Finset.mk with the nodup witness.

Русский

Для данного списка с повторениями, nodup, финсет эквивалентен Finset.mk.

LaTeX

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

Lean4

theorem toFinset_eq (n : Nodup l) : @Finset.mk α l n = l.toFinset :=
  Multiset.toFinset_eq <| by rwa [Multiset.coe_nodup]

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