English
EmbDomain extends the domain of HahnSeries by an order embedding f: Γ ↪o Γ', producing (embDomain f x) with coefficients pulled back along f.
Русский
EmbDomain расширяет область определения Hahn-рядов с помощью вложенного отображения порядка f: Γ ↪o Γ', создавая (embDomain f x) с коэффициентами, вытянутыми вдоль f.
LaTeX
$$$ (\\mathrm{embDomain}(f)\\,x).\\mathrm{coeff}(b) = \\begin{cases} x.\\mathrm{coeff}(a) & \\text{if } \\exists a: \\Gamma, b = f(a) \\text{ and } a \\in \\operatorname{supp}(x), \\\\ 0 & \\text{otherwise}. \\end{cases} $$$
Lean4
/-- Extends the domain of a `HahnSeries` by an `OrderEmbedding`. -/
def embDomain (f : Γ ↪o Γ') : HahnSeries Γ R → HahnSeries Γ' R := fun x =>
{ coeff := fun b : Γ' => if h : b ∈ f '' x.support then x.coeff (Classical.choose h) else 0
isPWO_support' :=
(x.isPWO_support.image_of_monotone f.monotone).mono fun b hb =>
by
contrapose! hb
rw [Function.mem_support, dif_neg hb, Classical.not_not] }
