mk_lf

Mathlib.SetTheory.PGame.Order

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

English

mk xl xr xL xR ⧏ xR j for any j.

Русский

mk xl xr xL xR ⧏ xR j для любого j.

LaTeX

$$$$ mk xl xr xL xR \\\\mathbf{⧏} xR j. $$$$

Lean4

theorem mk_lf {xl xr} (xL : xl → PGame) (xR : xr → PGame) (j) : mk xl xr xL xR ⧏ xR j :=
  @lf_moveRight (mk _ _ _ _) j

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

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

Разделы

Аффилиация

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