ofFn_degree_lt — Mathlib

English

For any v, deg(ofFn n v) < n.

Русский

Для любого v, deg(ofFn n v) < n.

LaTeX

$$$\deg(\operatorname{ofFn}(n)\, v) < n.$$$

Lean4

/-- `ofFn n v` has `degree` smaller than `n`. -/
theorem ofFn_degree_lt {n : ℕ} (v : Fin n → R) : (ofFn n v).degree < n :=
  by
  by_cases h : ofFn n v = 0
  · simp only [h, degree_zero]
    exact Batteries.compareOfLessAndEq_eq_lt.mp rfl
  ·
    exact
      (natDegree_lt_iff_degree_lt h).mp <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr <| ne_zero_of_ofFn_ne_zero h) _

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