toNat_lt_toNat

Mathlib.SetTheory.Cardinal.ToNat

URI: https://scilib.ai/kg/mathlib#Cardinal.toNat_lt_toNat

English

If c < d and d < aleph0, then toNat(c) < toNat(d).

Русский

Если c < d и d < ℵ0, то toNat(c) < toNat(d).

LaTeX

$$$\forall c,d\ (hc: c < d) (hd: d < \aleph_0),\ toNat(c) < toNat(d).$$$

Lean4

theorem toNat_lt_toNat (hcd : c < d) (hd : d < ℵ₀) : toNat c < toNat d :=
  toNat_strictMonoOn (hcd.trans hd) hd hcd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru