eq_mk_of_is_sol_of_eq_init' — Mathlib

English

If u is a solution to E and it matches init on the first E.order indices, then u equals E.mkSol init as a function.

Русский

Если u — решение E и оно совпадает с init на первых order индексов, то u равно функции E.mkSol init.

LaTeX

$$u = E.mkSol init$$

Lean4

/-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
  then `u = E.mkSol init`. This proves that `E.mkSol init` is the only solution
  of `E` whose first `E.order` values are given by `init`. -/
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) : u = E.mkSol init :=
  funext (E.eq_mk_of_is_sol_of_eq_init h heq)

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