card_eq — Mathlib

English

If α and β are finite, then card(α) = card(β) if and only if there exists a bijection α ≃ β.

Русский

Если α и β конечны, то card(α) = card(β) тогда и только тогда, когда существует биекция α ≃ β.

LaTeX

$$$Nat.card(\alpha) = Nat.card(\beta) \iff Nonempty(\alpha \cong \beta)$$$

Lean4

theorem card_eq [Finite α] [Finite β] : Nat.card α = Nat.card β ↔ Nonempty (α ≃ β) :=
  by
  haveI := Fintype.ofFinite α
  haveI := Fintype.ofFinite β
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq]

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