sub_lt_of_le

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

Let a, b, c be ordinals with b ≤ a. Then a − b < c if and only if a < b + c.

Русский

Пусть a, b, c — ординалы и b ≤ a. Тогда a − b < c тогда и только если a < b + c.

LaTeX

$$$\forall a,b,c\in\mathrm{Ord},\; b\le a\Rightarrow (a- b < c \iff a < b+c).$$$

Lean4

theorem sub_lt_of_le {a b c : Ordinal} (h : b ≤ a) : a - b < c ↔ a < b + c :=
  lt_iff_lt_of_le_iff_le (le_sub_of_le h)

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

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

Разделы

Аффилиация

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