le_weightedOrder — Mathlib

English

Let n be an extended natural; if every coefficient with weight below n is zero, then n ≤ weightedOrder_w(f).

Русский

Пусть n — расширенная натуральная; если все коэффициенты с весом меньше n равны нулю, тогда n ≤ weightedOrder_w(f).

LaTeX

$$$n \le f.weightedOrder w$$$

Lean4

/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
theorem le_weightedOrder {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, weight w d < n → coeff d f = 0) : n ≤ f.weightedOrder w :=
  by
  cases n
  · rw [top_le_iff, weightedOrder_eq_top_iff]
    ext d; exact h d (ENat.coe_lt_top _)
  · apply nat_le_weightedOrder; simpa only [ENat.some_eq_coe, Nat.cast_lt] using h

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