values_eq_on_of_interpolate_eq — Mathlib

English

If interpolate s v r = interpolate s v r', then r(i)=r'(i) for all i ∈ s

Русский

Если интерполяции совпадают, то значения совпадают на всех узлах

LaTeX

$$interpolate(s,v,r) = interpolate(s,v,r') \Rightarrow \forall i\in s, r(i)=r'(i)$$

Lean4

theorem values_eq_on_of_interpolate_eq (hvs : Set.InjOn v s) (hrr' : interpolate s v r = interpolate s v r') :
    ∀ i ∈ s, r i = r' i := fun _ hi => by
  rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' hvs hi]

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