coeff_coe_trunc_of_lt — Mathlib

English

If n < m, then the n-th coefficient of trunc m f equals the n-th coefficient of f.

Русский

Если n < m, то n-й коэффициент trunc m f равен n‑му коэффициенту f.

LaTeX

$$$\\forall {n,m}, \\; n < m \\Rightarrow \\operatorname{coeff} n (\\operatorname{trunc} m f) = \\operatorname{coeff} n f$$$

Lean4

/-- The function `coeff n : R⟦X⟧ → R` is continuous. I.e. `coeff n f` depends only on a sufficiently
long truncation of the power series `f`. -/
theorem coeff_coe_trunc_of_lt {n m} {f : R⟦X⟧} (h : n < m) : coeff n (trunc m f) = coeff n f := by
  rwa [coeff_coe, coeff_trunc, if_pos]

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