truncOfCardPos — Mathlib

English

If a finite type α has positive cardinality, then there exists a constructive element of α (a truncation).

Русский

Если кардинальность конечного типа α положительна, существует конструктивный элемент α в виде трunc.

LaTeX

$$$0 < |\alpha| \Rightarrow \mathrm{Trunc}(\alpha)$$$

Lean4

/-- A `Fintype` with positive cardinality constructively contains an element.
-/
def truncOfCardPos {α} [Fintype α] (h : 0 < Fintype.card α) : Trunc α :=
  letI := Fintype.card_pos_iff.mp h
  truncOfNonemptyFintype α

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