ofStateAuxRelabelling — Mathlib

English

Two valid bounds n,m give relabellings between the corresponding ofStateAux games.

Русский

Два допустимых значения границы n,m дают взаимно однозначные соответствия между играми ofStateAux(n) и ofStateAux(m).

LaTeX

$$$\forall s,n,m,\ hn,hm:\ turnBound s ≤ n \land turnBound s ≤ m \Rightarrow Relabelling( ofStateAux(n,s,hn) )( ofStateAux(m,s,hm) )$$$

Lean4

/-- Two different (valid) turn bounds give equivalent games. -/
def ofStateAuxRelabelling :
    ∀ (s : S) (n m : ℕ) (hn : turnBound s ≤ n) (hm : turnBound s ≤ m),
      Relabelling (ofStateAux n s hn) (ofStateAux m s hm)
  | s, 0, 0, hn, hm => by
    dsimp [PGame.ofStateAux]
    fconstructor
    · rfl
    · rfl
    · intro i; dsimp at i; exfalso
      exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
    · intro j; dsimp at j; exfalso
      exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
  | s, 0, m + 1, hn, hm => by
    dsimp [PGame.ofStateAux]
    fconstructor
    · rfl
    · rfl
    · intro i; dsimp at i; exfalso
      exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
    · intro j; dsimp at j; exfalso
      exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hn)
  | s, n + 1, 0, hn, hm => by
    dsimp [PGame.ofStateAux]
    fconstructor
    · rfl
    · rfl
    · intro i; dsimp at i; exfalso
      exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hm)
    · intro j; dsimp at j; exfalso
      exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
  | s, n + 1, m + 1, hn, hm => by
    dsimp [PGame.ofStateAux]
    fconstructor
    · rfl
    · rfl
    · intro i
      apply ofStateAuxRelabelling
    · intro j
      apply ofStateAuxRelabelling

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