mkSol_eq_init — Mathlib

English

If u is a solution of E and its first E.order values agree with init, then for every n, u(n) equals E.mkSol init(n).

Русский

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

LaTeX

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

Lean4

/-- `E.mkSol init`'s first `E.order` terms are `init`. -/
theorem mkSol_eq_init (init : Fin E.order → R) : ∀ n : Fin E.order, E.mkSol init n = init n :=
  by
  intro n
  rw [mkSol]
  simp only [n.is_lt, dif_pos, Fin.mk_val]

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