natCast_toNat_le

Mathlib.SetTheory.Cardinal.ToNat

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

← MathLib Explorer

English

For every cardinal a, (toNat(a) as a cardinal) ≤ a.

Русский

Для любого кардинала a: (toNat(a) как кардинал) ≤ a.

LaTeX

$$$(\operatorname{toNat}(a) : \mathrm{Cardinal}) \le a.$$$

Lean4

@[simp]
theorem natCast_toNat_le (a : Cardinal) : (toNat a : Cardinal) ≤ a :=
  by
  obtain h | h := lt_or_ge a ℵ₀
  · simp [cast_toNat_of_lt_aleph0 h]
  · simp [Cardinal.toNat_apply_of_aleph0_le h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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