eval_interpolate_at_node — Mathlib

English

If injOn v on s, then eval (v(i)) of interpolate s v r equals r(i) for i ∈ s.

Русский

Если injOn v на s выполняется, то значение на узле i: eval(v(i), interpolate s v r) = r(i).

LaTeX

$$$\operatorname{eval}(v(i), \text{interpolate}(s,v,r)) = r(i)\quad (i\in s)$$

Lean4

theorem eval_interpolate_at_node (hvs : Set.InjOn v s) (hi : i ∈ s) : eval (v i) (interpolate s v r) = r i :=
  by
  rw [interpolate_apply, eval_finset_sum, ← add_sum_erase _ _ hi]
  simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_eq_left]
  refine sum_eq_zero fun j H => ?_
  rw [eval_basis_of_ne (mem_erase.mp H).1 hi, mul_zero]

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