English
Let p be a subset of a type α. If there exists a finite Finset s of α such that the elements of s are exactly p (i.e., ∀x, x ∈ s ↔ x ∈ p), then p carries a natural fintype structure via the subtype construction.
Русский
Пусть p ⊆ α. Если существует конечный Finset s ⊆ α, чьи элементы совпадают с p (то есть ∀x, x ∈ s ↔ x ∈ p), тогда p получает естественную структуру конечного типа через подтип.
LaTeX
$$$\exists s:\mathrm{Finset}(\alpha),\ (\forall x:\alpha, x\in s \iff x\in p) \Rightarrow \text{Finite}(p).$$$
Lean4
/-- Construct a fintype from a finset with the same elements. -/
def ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : Fintype p :=
Fintype.subtype s H
