sub_eq_zero_iff_le

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

For ordinals a,b, a − b = 0 if and only if a ≤ b.

Русский

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

LaTeX

$$$a - b = 0 \iff a \le b$$$

Lean4

protected theorem sub_eq_zero_iff_le {a b : Ordinal} : a - b = 0 ↔ a ≤ b :=
  ⟨fun h => by simpa only [h, add_zero] using le_add_sub a b, fun h => by rwa [← Ordinal.le_zero, sub_le, add_zero]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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