lt_one_iff_zero

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.lt_one_iff_zero

English

o < 1 iff o = 0.

Русский

o < 1 тогда и только тогда, когда o = 0.

LaTeX

$$$o < 1 \\iff o = 0$$$

Lean4

@[simp]
theorem lt_one_iff_zero {o : NatOrdinal} : o < 1 ↔ o = 0 :=
  Ordinal.lt_one_iff_zero

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

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

Разделы

Аффилиация

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