toNat_lt_iff_lt_of_lt_aleph0 — Mathlib

English

For finite cardinals c,d (c < aleph0 and d < aleph0), we have toNat(c) < toNat(d) iff 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

theorem toNat_lt_iff_lt_of_lt_aleph0 (hc : c < ℵ₀) (hd : d < ℵ₀) : toNat c < toNat d ↔ c < d :=
  toNat_strictMonoOn.lt_iff_lt hc hd

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