English
For every i ∈ X and every n ∈ ℕ, the nth and (n+1)th approximations sCorec f i n and sCorec f i (succ n) agree; in other words, consecutive approximations are compatible.
Русский
Пусть для каждого i ∈ X и каждого n ∈ ℕ выполнено: приближение sCorec f i n и приближение sCorec f i (n+1) согласованы; то есть последовательные приближения совместимы.
LaTeX
$$$\\displaystyle \\forall i:\\, X\\,\\forall n:\\,\\mathbb{N},\\quad \\mathrm{Agree}\\bigl( sCorec\\ f\\ i\\ n,\\ sCorec\\ f\\ i\\ (\\operatorname{succ} n)\\bigr).$$$
Lean4
theorem P_corec (i : X) (n : ℕ) : Agree (sCorec f i n) (sCorec f i (succ n)) := by
induction n generalizing i with
| zero => constructor
| succ n n_ih =>
obtain ⟨y, g⟩ := f i
constructor
introv
apply n_ih
