two_le_iff_one_lt

Mathlib.SetTheory.Cardinal.Basic

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

English

The cardinal 2 is less than or equal to aleph-null if and only if 1 is less than aleph-null.

Русский

Кардинал 2 ограничен сверху или равен aleph-null тогда, когда 1 < aleph-null.

LaTeX

$$$2 \le \aleph_0 \iff 1 < \aleph_0$$$

Lean4

theorem two_le_iff_one_lt {c : Cardinal} : 2 ≤ c ↔ 1 < c :=
  by
  convert natCast_add_one_le_iff
  norm_cast

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

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

Разделы

Аффилиация

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