toPGame_lt_iff

Mathlib.SetTheory.Game.Ordinal

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

← MathLib Explorer

English

For any ordinals a and b, a.toPGame < b.toPGame if and only if a < b.

Русский

Пусть a и b — ординалы. Тогда a.toPGame < b.toPGame тогда и только тогда, когда a < b.

LaTeX

$$$a.toPGame < b.toPGame \iff a < b$$$

Lean4

@[simp]
theorem toPGame_lt_iff {a b : Ordinal} : a.toPGame < b.toPGame ↔ a < b :=
  ⟨by contrapose; rw [not_lt]; exact fun h => not_lt_of_ge (toPGame_le h), toPGame_lt⟩

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

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

Разделы

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

Аффилиация

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