natCast_add_one_le_iff

Mathlib.SetTheory.Cardinal.Basic

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

English

For natural n and a cardinal c, n+1 ≤ c if and only if n < c.

Русский

Для натурального n и кардинала c верно: n+1 ≤ c тогда и только если n < c.

LaTeX

$$$n + 1 \le c \iff n < c$$$

Lean4

theorem natCast_add_one_le_iff {n : ℕ} {c : Cardinal} : n + 1 ≤ c ↔ n < c := by
  rw [← Order.succ_le_iff, Cardinal.succ_natCast]

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

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

Разделы

Аффилиация

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