basis_ne_zero — Mathlib

English

If v is injective on s and i ∈ s, then the basis polynomial L_s,v,i is nonzero.

Русский

Если отображение v на области s инъективно и i ∈ s, то базисный многочлен L_s,v,i не равен нулю.

LaTeX

$$$L_s,v,i \neq 0$ при $i \in s$ и $v|_s$ инъективно$$

Lean4

theorem basis_ne_zero (hvs : Set.InjOn v s) (hi : i ∈ s) : Lagrange.basis s v i ≠ 0 :=
  by
  simp_rw [Lagrange.basis, prod_ne_zero_iff, Ne, mem_erase]
  rintro j ⟨hij, hj⟩
  rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]
  exact hij.symm

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