results_thinkN — Mathlib

English

Let s be a computation producing a at step m. For every n, if Results s a m holds, then Results (thinkN s n) a (m+n) holds.

Русский

Пусть s — вычисление, дающее a на шаге m. Тогда для любого n, если Results s a m, то Results (thinkN s n) a (m+n).

LaTeX

$$$$ \forall n,\ \operatorname{Results} s a m \rightarrow \operatorname{Results}(\mathrm{thinkN}\,s\,n)\ a\ (m+n). $$$$

Lean4

theorem results_thinkN {s : Computation α} {a m} : ∀ n, Results s a m → Results (thinkN s n) a (m + n)
  | 0, h => h
  | n + 1, h => results_think (results_thinkN n h)

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