eq_interpolate — Mathlib

English

Equality of interpolations characterized by degree bound and evaluation conditions.

Русский

Уравнивание интерполяций характеризуется ограничением степени и условиями значений.

LaTeX

$$eq_interpolate {f : F[X]} (hvs) (degree_f_lt) (eval_f) : f = interpolate s v r$$

Lean4

theorem eq_interpolate {f : F[X]} (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s) :
    f = interpolate s v fun i => f.eval (v i) :=
  eq_of_degrees_lt_of_eval_index_eq _ hvs degree_f_lt (degree_interpolate_lt _ hvs) fun _ hi =>
    (eval_interpolate_at_node (fun x ↦ eval (v x) f) hvs hi).symm

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