is_sol_mkSol — Mathlib

English

For any initial data init, the sequence E.mkSol(init) satisfies the recurrence E; that is, it is a solution of E.

Русский

Для любых начальных данных init последовательность E.mkSol(init) удовлетворяет рекуррентности E; она является её решением.

LaTeX

$$$E.IsSolution(E.mkSol\, init)$$$

Lean4

/-- `E.mkSol` indeed gives solutions to `E`. -/
theorem is_sol_mkSol (init : Fin E.order → R) : E.IsSolution (E.mkSol init) :=
  by
  intro n
  rw [mkSol]
  simp

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