sub_eq_of_add_eq

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

If a + b = c, then c − a = b.

Русский

Если a + b = c, то c − a = b.

LaTeX

$$$\forall a\,\forall b\,\forall c:\; (a + b = c) \Rightarrow (c - a = b).$$$

Lean4

theorem sub_eq_of_add_eq {a b c : Ordinal} (h : a + b = c) : c - a = b :=
  h ▸ add_sub_cancel _ _

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

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

Разделы

Аффилиация

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