turnBound_of_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem turnBound_of_left {s t : S} (m : t ∈ l s) (n : ℕ) (h : turnBound s ≤ n + 1) : turnBound t ≤ n :=
  Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (left_bound m) h)

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