le_stable — Mathlib

English

Let s be a computation. If m ≤ n and the m-th value equals some a, then the n-th value also equals the same a.

Русский

Пусть s — вычисление. Если m ≤ n и значение на позиции m равно Some(a), то на позиции n оно также равно Some(a).

LaTeX

$$$\forall s:\\ Computation\,\alpha\; \forall a\, m\, n,\; m \le n \rightarrow s.1\,m = \text{some } a \rightarrow s.1\,n = \text{some } a$$$

Lean4

theorem le_stable (s : Computation α) {a m n} (h : m ≤ n) : s.1 m = some a → s.1 n = some a :=
  by
  obtain ⟨f, al⟩ := s
  induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

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