ofSuppBddBelow — Mathlib

English

From any function with bounded-below support, construct a Hahn series with those coefficients.

Русский

Из любой функции с ограниченной снизу опорой строится Hahn-ряд с этими коэффициентами.

LaTeX

$$ofSuppBddBelow (f) (hf) : HahnSeries Γ R where coeff := f; isPWO_support' := suppBddBelow_supp_PWO f hf$$

Lean4

/-- Construct a Hahn series from any function whose support is bounded below. -/
@[simps]
def ofSuppBddBelow (f : Γ → R) (hf : BddBelow (Function.support f)) : HahnSeries Γ R
    where
  coeff := f
  isPWO_support' := suppBddBelow_supp_PWO f hf

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