moveRight

Mathlib.SetTheory.Surreal.Basic

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

English

If x' is an option of x and x is numeric, then x' is numeric.

Русский

Если x' является опцией x и x числовая, то x' числовая.

LaTeX

$$$x' \text{IsOption } x \Rightarrow x \text{ Numeric } \Rightarrow x' \text{ Numeric }$$$

Lean4

theorem moveRight {x : PGame} (o : Numeric x) (j : x.RightMoves) : Numeric (x.moveRight j) := by cases x; exact o.2.2 j

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

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

Разделы

Аффилиация

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