natDegree_trunc_lt — Mathlib

English

For any f and n, the natural degree of trunc(n+1) f is strictly less than n+1.

Русский

Для любого f и n натуральная степень trunc(n+1) fStrict меньше n+1.

LaTeX

$$$\\operatorname{natDegree}(\\operatorname{trunc}(n+1) f) < n+1$$$

Lean4

theorem natDegree_trunc_lt (f : R⟦X⟧) (n) : (trunc (n + 1) f).natDegree < n + 1 :=
  by
  rw [Nat.lt_succ_iff, natDegree_le_iff_coeff_eq_zero]
  intros
  rw [coeff_trunc]
  split_ifs with h
  · rw [lt_succ, ← not_lt] at h
    contradiction
  · rfl

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