toPGame_lf

Mathlib.SetTheory.Game.Ordinal

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

English

If a < b then a.toPGame ⧏ b.toPGame (left-fraction relation).

Русский

Если a < b, то a.toPGame ⧏ b.toPGame (отношение левой части).

LaTeX

$$$a.toPGame \\;\\\\text{LF}\\\\; b.toPGame.$$$

Lean4

theorem toPGame_lf {a b : Ordinal} (h : a < b) : a.toPGame ⧏ b.toPGame := by
  convert moveLeft_lf (toLeftMovesToPGame ⟨a, h⟩); rw [toPGame_moveLeft]

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

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

Разделы

Аффилиация

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