toNat_le_toNat

Mathlib.SetTheory.Cardinal.ToNat

URI: https://scilib.ai/kg/mathlib#Cardinal.toNat_le_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 \le d) (hd: d < \aleph_0),\ toNat(c) \le toNat(d).$$$

Lean4

@[gcongr]
theorem toNat_le_toNat (hcd : c ≤ d) (hd : d < ℵ₀) : toNat c ≤ toNat d :=
  toNat_monotoneOn (hcd.trans_lt hd) hd hcd

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

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

Разделы

Аффилиация

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