fintype — Mathlib

English

Equivalent formulation: a set is finite iff there exists a finite type on its elements.

Русский

Эквивалентная формулировка: множество конечное тогда и только тогда, когда его элементы образуют конечный тип.

LaTeX

$$$$ s.Finite \\iff \\exists \\text{Fintype}(s). $$$$

Lean4

/-- A finite set coerced to a type is a `Fintype`.
This is the `Fintype` projection for a `Set.Finite`.

Note that because `Finite` isn't a typeclass, this definition will not fire if it
is made into an instance -/
protected noncomputable def fintype {s : Set α} (h : s.Finite) : Fintype s :=
  h.nonempty_fintype.some

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