coeff_truncLT_of_le — Mathlib

English

Let [Zero Γ], f : Γ → R with f ≠ 0, n : Γ and hn : ∀ m < n, f m = 0. Then n ≤ order(ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)).

Русский

Пусть [Zero Γ], f : Γ → R, f ≠ 0, n ∈ Γ и hn: для всех m < n, f m = 0. Тогда n ≤ order(ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)).

LaTeX

$$n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn))$$

Lean4

theorem coeff_truncLT_of_le [LinearOrder Γ] {c i : Γ} (h : c ≤ i) (x : HahnSeries Γ R) : (truncLT c x).coeff i = 0 := by
  simp [h]

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