finite_def — Mathlib

English

A set is finite if and only if its carrier is a finite type (i.e., there exists a fintype structure on the set).

Русский

Множество считается конечным тогда и только тогда, когда множество как тип имеет конечный каркас (существует структура fintype на множестве).

LaTeX

$$$$ s.Finite \\iff Nonempty(\\mathrm{Fintype}\\ s). $$$$

Lean4

theorem finite_def {s : Set α} : s.Finite ↔ Nonempty (Fintype s) :=
  finite_iff_nonempty_fintype s

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