toPGame_lf_iff — Mathlib

English

For all ordinals a and b, the left-forcing relation between their toPGame images holds precisely when a < b: a.toPGame ⧏ b.toPGame iff a < b.

Русский

Пусть a и b — ординалы. Тогда отношение LF между a.toPGame и b.toPGame верно тогда и только тогда, когда a < b.

LaTeX

$$$(a.toPGame) \mathrm{LF} (b.toPGame) \iff a < b$$$

Lean4

@[simp]
theorem toPGame_lf_iff {a b : Ordinal} : a.toPGame ⧏ b.toPGame ↔ a < b :=
  ⟨by contrapose; rw [not_lt, not_lf]; exact toPGame_le, toPGame_lf⟩

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