toFinset — Mathlib

English

For any set s with a finiteness structure, toFinset s yields a finite enumeration of its elements as a Finset.

Русский

Для множества s с конечной структурой, toFinset s образует конечную упорядоченную перечень его элементов в Finset.

LaTeX

$$$\mathrm{toFinset}\;s = \text{Finset of elements of } s$$$

Lean4

/-- Construct a finset enumerating a set `s`, given a `Fintype` instance. -/
def toFinset (s : Set α) [Fintype s] : Finset α :=
  (@Finset.univ s _).map <| Function.Embedding.subtype _

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