turnBound_of_right — Mathlib

English

If s has a right move to t, then turnBound(t) ≤ turnBound(s) − 1 under turnBound(s) ≤ n+1.

Русский

Если у s есть правый ход к t, то при условии turnBound(s) ≤ n+1 выполняется turnBound(t) ≤ n.

LaTeX

$$$ \forall {s,t},\ m : t\in r(s) \Rightarrow \forall n,\ turnBound(s) \le n+1 \Rightarrow turnBound(t) \le n $$$

Lean4

theorem turnBound_of_right {s t : S} (m : t ∈ r s) (n : ℕ) (h : turnBound s ≤ n + 1) : turnBound t ≤ n :=
  Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (right_bound m) h)

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