turnBound_ne_zero_of_left_move — Mathlib

English

If t is a left move from s, then turnBound(s) ≠ 0; a left move cannot exist when bound is zero.

Русский

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

LaTeX

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

Lean4

theorem turnBound_ne_zero_of_left_move {s t : S} (m : t ∈ l s) : turnBound s ≠ 0 :=
  by
  intro h
  have t := left_bound m
  rw [h] at t
  exact Nat.not_succ_le_zero _ t

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