instIsRightCancelAdd

Mathlib.SetTheory.Nimber.Basic

URI: https://scilib.ai/kg/mathlib#Nimber.instIsRightCancelAdd

← MathLib Explorer

English

Addition in Nimbers is right-cancellative: if x + a = y + a, then x = y.

Русский

Сложение Nimbers справа карательно: если x + a = y + a, значит x = y.

LaTeX

$$IsRightCancelAdd Nimber$$

Lean4

instance : IsRightCancelAdd Nimber := by
  constructor
  intro a b c h
  apply le_antisymm <;> apply le_of_not_gt
  · exact fun hc => (add_ne_of_lt b a).1 c hc h.symm
  · exact fun ha => (add_ne_of_lt c a).1 b ha h

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

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

Разделы

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

Аффилиация

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