toFinset — Mathlib

English

There is a canonical Finite-type structure on a finite set viewed as a Set.

Русский

Для конечного множества, рассмотренного как множество, существует каноническая структура конечного типа.

LaTeX

$$$$ \\mathrm{Set.Finite}.fintype : s.Finite \\Rightarrow \\mathrm{Fintype}(s). $$$$

Lean4

/-- Using choice, get the `Finset` that represents this `Set`. -/
protected noncomputable def toFinset {s : Set α} (h : s.Finite) : Finset α :=
  @Set.toFinset _ _ h.fintype

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