eval — Mathlib

English

Promoting eval coefficients to HahnSeries yields a well-defined Lex-ordered series with the correct support.

Русский

Преобразование коэффициентов eval в ряд Хаана образует корректный Lex-ряд с поддержкой.

LaTeX

$$$\text{evalCoeff}$ promotes to $\text{Lex}(\text{HahnSeries})$ with correct support$$

Lean4

/-- Promote `HahnEmbedding.Partial.evalCoeff`'s output to a new `HahnSeries`. -/
noncomputable def eval [IsOrderedAddMonoid R] [Archimedean R] (x : M) : Lex (HahnSeries (FiniteArchimedeanClass M) R) :=
  toLex
    { coeff := f.evalCoeff x
      isPWO_support' := (f.isWF_support_evalCoeff x).isPWO }

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