Supremum mapping?

Stream: new members

[Tristan Figueroa-Reid]

I'm trying to work on the theory of dominated pre-games, and got stuck here:

def undominateLeft: PGame → PGame
  | mk L R l r => ⟨ ??, R, l, r ⟩

Essentially, it's supposed to make a game no longer dominated. This is the definition of a game being left dominated (as I presume that right domination and bi-domination follows)

/-- A game is left-dominatable if distinct elements in its left moves are comparable. -/
def LeftDomaintable (x : PGame) : Prop :=
  ∃ (l₁ : LeftMoves x), ∃ (l₂ : LeftMoves x), x.moveLeft l₁ ≡ x.moveLeft l₂ ∨
    x.moveLeft l₁ ≤ x.moveLeft l₂

...

theorem undominateLeftNonDominatable (x : PGame) : ¬ (LeftDomaintable (undominateLeft x)) := by sorry

I would like to do something like "restrict L to only be the type of variables that are in the supremum set of l m for every m: L," but I have little clue where to start.