sub_ne_zero_iff_lt

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.sub_ne_zero_iff_lt

English

For ordinals a,b, a − b ≠ 0 if and only if b < a.

Русский

Для ординалов a,b: a − b ≠ 0 тогда и только если b < a.

LaTeX

$$$a - b \neq 0 \iff b < a$$$

Lean4

protected theorem sub_ne_zero_iff_lt {a b : Ordinal} : a - b ≠ 0 ↔ b < a := by
  simpa using Ordinal.sub_eq_zero_iff_le.not

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

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

Разделы

Аффилиация

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