equivFinOfCardPos — Mathlib

English

If a type α has nonzero cardinality, then there is an equivalence α ≃ Fin(card α).

Русский

Если кардинальность α ненулевая, существует биекция α ≃ Fin(card α).

LaTeX

$$$$ \alpha \cong Fin(\operatorname{card}(\alpha)) \quad \text{when } \operatorname{card}(\alpha) \neq 0 $$$$

Lean4

/-- If the cardinality is positive, that means it is a finite type, so there is
an equivalence between `α` and `Fin (Nat.card α)`. See also `Finite.equivFin`. -/
def equivFinOfCardPos {α : Type*} (h : Nat.card α ≠ 0) : α ≃ Fin (Nat.card α) :=
  by
  cases fintypeOrInfinite α
  · simpa only [card_eq_fintype_card] using Fintype.equivFin α
  · simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h

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