instIsTrichotomousLF

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.Game.instIsTrichotomousLF

English

For any x,y in Game, exactly one of x ≤ y, x ≈ y, or y ≤ x holds.

Русский

Для любых x,y в игре верно, что либо x ≤ y, либо x ≈ y, либо y ≤ x.

LaTeX

$$$ x \le y \lor x \approx y \lor y \le x $$$

Lean4

instance : IsTrichotomous Game LF :=
  ⟨by
    rintro ⟨x⟩ ⟨y⟩
    change _ ∨ ⟦x⟧ = ⟦y⟧ ∨ _
    rw [Quotient.eq]
    apply lf_or_equiv_or_gf⟩

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

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

Разделы

Аффилиация

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