eval_basis_self — Mathlib

English

Evaluating the i-th Lagrange basis at v_i yields 1, provided injOn v on s.

Русский

Значение базиса L_s,v,i в точке v_i равно 1, если v инъективно на s.

LaTeX

$$$(L_s,v,i)(v_i)=1$$$

Lean4

@[simp]
theorem eval_basis_self (hvs : Set.InjOn v s) (hi : i ∈ s) : (Lagrange.basis s v i).eval (v i) = 1 :=
  by
  rw [Lagrange.basis, eval_prod]
  refine prod_eq_one fun j H => ?_
  rw [eval_basisDivisor_left_of_ne]
  rcases mem_erase.mp H with ⟨hij, hj⟩
  exact mt (hvs hi hj) hij.symm

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