fintypeOrInfinite — Mathlib

English

Every type is classically either finite or infinite.

Русский

Каждый тип классифицируется классически как конечный или бесконечный.

LaTeX

$$$\\text{Finite}(\\alpha) \\lor \\operatorname{Infinite}(\\alpha)$$$

Lean4

/-- Any type is (classically) either a `Fintype`, or `Infinite`.

One can obtain the relevant typeclasses via `cases fintypeOrInfinite α`.
-/
noncomputable def fintypeOrInfinite (α : Type*) : Fintype α ⊕' Infinite α :=
  if h : Infinite α then PSum.inr h else PSum.inl (fintypeOfNotInfinite h)

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