eq_mk_of_is_sol_of_eq_init — Mathlib

English

If u is a solution of E and it agrees with init on the first E.order entries, then u(n) = E.mkSol init(n) for all n.

Русский

Если u — решение E и согласуется с init на первых E.order членах, то u(n) = E.mkSol init(n) для всех n.

LaTeX

$$$\forall n,\ u(n) = E.mkSol init\, n$$$

Lean4

/-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
  then `∀ n, u n = E.mkSol init n`. -/
theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → R} {init : Fin E.order → R} (h : E.IsSolution u)
    (heq : ∀ n : Fin E.order, u n = init n) : ∀ n, u n = E.mkSol init n :=
  by
  intro n
  rw [mkSol]
  split_ifs with h'
  · exact mod_cast heq ⟨n, h'⟩
  · dsimp only
    rw [← tsub_add_cancel_of_le (le_of_not_gt h'), h (n - E.order)]
    congr with k
    rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
    simp

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