AllAgree — Mathlib

English

AllAgree(x) asserts that the approximations x(n) and x(n+1) agree for every n.

Русский

AllAgree(x) утверждает, что аппроксимации x(n) и x(n+1) согласуются для каждого n.

LaTeX

$$$\text{AllAgree} (x) :\, \forall n,\, \text{Agree}(x(n), x(n+1)).$$$

Lean4

/-- Given an infinite series of approximations `approx`,
`AllAgree approx` states that they are all consistent with each other.
-/
def AllAgree (x : ∀ n, CofixA F n) :=
  ∀ n, Agree (x n) (x (succ n))

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