card_eq_nat — Mathlib

English

For ordinal o and natural n, card(o) = n ↔ o = n, i.e., the only way a finite ordinal o has cardinality n is when o equals the finite ordinal n.

Русский

Для ординала o и натурального n, card(o) = n ↔ o = n; то есть ровно тогда, когда ординал o равен конечному ординалу n, кардинал равен n.

LaTeX

$$$\forall o\,\forall n\in\mathbb{N},\; \operatorname{card}(o) = n \iff o = n$$$

Lean4

@[simp]
theorem card_eq_nat {o} {n : ℕ} : card o = n ↔ o = n := by simp only [le_antisymm_iff, card_le_nat, nat_le_card]

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