toNat_inj_of_lt_aleph0 — Mathlib

English

For finite cardinals c and d (i.e., c < aleph0 and d < aleph0), toNat(c) = toNat(d) if and only if c = d.

Русский

Для конечных кардиналов c и d (c < ℵ0 и d < ℵ0) имеет место: toNat(c) = toNat(d) тогда и только тогда, когда c = d.

LaTeX

$$$\forall c,d \in Iio(\aleph_0): \operatorname{toNat}(c) = \operatorname{toNat}(d) \iff c = d.$$$

Lean4

/-- Two finite cardinals are equal
iff they are equal their `Cardinal.toNat` projections are equal. -/
theorem toNat_inj_of_lt_aleph0 (hc : c < ℵ₀) (hd : d < ℵ₀) : toNat c = toNat d ↔ c = d :=
  toNat_injOn.eq_iff hc hd

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