degree_interpolate_erase_lt — Mathlib

English

Removing i from s yields interpolate(s\{i}) has degree < (#s − 1)

Русский

Удаление i из s даёт интерполяцию по s\{i} степени меньше чем (#s − 1)

LaTeX

$$deg(\text{interpolate}(s\setminus {i},v,r)) < (|s|-1)$$

Lean4

theorem degree_interpolate_erase_lt (hvs : Set.InjOn v s) (hi : i ∈ s) :
    (interpolate (s.erase i) v r).degree < ↑(#s - 1) :=
  by
  rw [← Finset.card_erase_of_mem hi]
  exact degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)

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