turnBound_ne_zero_of_right_move

Mathlib.SetTheory.Game.State

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.turnBound_ne_zero_of_right_move

English

If t is a right move from s, then turnBound(s) ≠ 0.

Русский

Если t является правым ходом из s, то turnBound(s) ≠ 0.

LaTeX

$$$ \forall {s,t},\ t\in r(s) \Rightarrow turnBound(s) \neq 0 $$$

Lean4

theorem turnBound_ne_zero_of_right_move {s t : S} (m : t ∈ r s) : turnBound s ≠ 0 :=
  by
  intro h
  have t := right_bound m
  cutsat

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

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

Разделы

Аффилиация

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