card_eq — Mathlib

English

Two types have the same finite cardinality if and only if there exists an equivalence between them.

Русский

У двух типов одинаковая конечная мощность тогда и только тогда, когда существует эквиваленция между ними.

LaTeX

$$$\operatorname{card}\alpha = \operatorname{card}\beta \iff \exists e:\alpha \simeq \beta.$$$

Lean4

theorem card_eq {α β} [_F : Fintype α] [_G : Fintype β] : card α = card β ↔ Nonempty (α ≃ β) :=
  ⟨fun h =>
    haveI := Classical.propDecidable
    (truncEquivOfCardEq h).nonempty,
    fun ⟨f⟩ => card_congr f⟩

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