sub

Mathlib.SetTheory.Surreal.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Numeric.sub

English

If x and y are numeric, then x − y is numeric.

Русский

Если x и y числовые, то x − y числовое.

LaTeX

$$$(\forall x,y, Numeric(x) \land Numeric(y)) \Rightarrow Numeric(x - y)$$$

Lean4

theorem sub {x y : PGame} (ox : Numeric x) (oy : Numeric y) : Numeric (x - y) :=
  ox.add oy.neg

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

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

Разделы

Аффилиация

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