succ_ne_zero

Mathlib.SetTheory.Cardinal.Order

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

English

For every cardinal c, succ(c) ≠ 0. The successor is never zero.

Русский

Для любого кардинала c, succ(c) ≠ 0. Преемник никогда не ноль.

LaTeX

$$$\\operatorname{succ}(c) \\neq 0$$$

Lean4

theorem succ_ne_zero (c : Cardinal) : succ c ≠ 0 :=
  (succ_pos _).ne'

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

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

Разделы

Аффилиация

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