truncLT — Mathlib

English

For i < c, the truncation keeps coefficients intact: (truncLT c x).coeff i = x.coeff i.

Русский

Для i < c коэффициенты сохраняются: (truncLT c x).coeff i = x.coeff i.

LaTeX

$$(truncLT c x).coeff i = x.coeff i$$

Lean4

/-- Zeroes out coefficients of a `HahnSeries` at indices not less than `c`. -/
def truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) : ZeroHom (HahnSeries Γ R) (HahnSeries Γ R)
    where
  toFun
    x :=
    { coeff i := if i < c then x.coeff i else 0
      isPWO_support' := Set.IsPWO.mono x.isPWO_support (by simp) }
  map_zero' := by ext; simp

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