instIsLeftCancelAdd

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

Left cancellation of addition holds for ordinals: if a + b = a + c then b = c.

Русский

Слева отменяется сложение для ординалов: если a + b = a + c, то b = c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ a+b = a+c \Rightarrow b=c$$$

Lean4

instance : IsLeftCancelAdd Ordinal where
  add_left_cancel a b c h := by simpa only [le_antisymm_iff, add_le_add_iff_left] using h

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

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

Разделы

Аффилиация

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