toFinset — Mathlib

English

toFinset l is the Finset formed from the elements of the list l by removing duplicates.

Русский

toFinset l — это Finset, состоящее из элементов списка l после удаления повторов.

LaTeX

$$$\\text{toFinset}(l) = \\mathsf{Finset}\\alpha$-множество элементов списка $l$ без повторов$$

Lean4

/-- `toFinset l` removes duplicates from the list `l` to produce a finset. -/
def toFinset (l : List α) : Finset α :=
  Multiset.toFinset l

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