terminated_stable — Mathlib

English

If g is terminated at n, then contsAux(n+2) = contsAux(n+1).

Русский

Если g завершилось на позиции n, contsAux(n+2) = contsAux(n+1).

LaTeX

$$$$\text{contsAux}(n+2) = \text{contsAux}(n+1)\quad\text{when } \text{TerminatedAt}(g,n).$$$$

Lean4

/-- If a gcf terminated at position `n`, it also terminated at `m ≥ n`. -/
theorem terminated_stable (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.TerminatedAt m :=
  g.s.terminated_stable n_le_m terminatedAt_n

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