toPGame_le_iff

Mathlib.SetTheory.Game.Ordinal

URI: https://scilib.ai/kg/mathlib#Ordinal.toPGame_le_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 \le b.toPGame \iff a \le b$$$

Lean4

@[simp]
theorem toPGame_le_iff {a b : Ordinal} : a.toPGame ≤ b.toPGame ↔ a ≤ b :=
  ⟨by contrapose; rw [not_le, PGame.not_le]; exact toPGame_lf, toPGame_le⟩

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

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

Разделы

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

Аффилиация

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