interpolate_eq_iff_values_eq_on — Mathlib

English

For any f ∈ F[X], if hvs and degree_f_lt hold, then f = interpolate s v (f.eval ∘ v).

Русский

Для любого f ∈ F[X] при выполнении условий hvs и degree_f_lt верно f = interpolate s v (функция eval ∘ v).

LaTeX

$$f = \text{interpolate}(s,v,\lambda i. f(v(i)))$$

Lean4

theorem interpolate_eq_iff_values_eq_on (hvs : Set.InjOn v s) :
    interpolate s v r = interpolate s v r' ↔ ∀ i ∈ s, r i = r' i :=
  ⟨values_eq_on_of_interpolate_eq _ _ hvs, interpolate_eq_of_values_eq_on _ _⟩

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