English
Change a Hahn series with coefficients in HahnSeries Γ' R to a HahnSeries on the Lex product; the coefficient at g = (g1,g2) equals the coefficient at g1 of the inner HahnSeries evaluated at g2.
Русский
Преобразование ряда Хана, коэффициенты которого лежат в HahnSeries Γ' R, в ряд на лексикографическом произведении; коэффициент при g = (g1,g2) равен коэффициенту при g2 в (коэффициент x g1).
LaTeX
$$$\\text{ofIterate} : HahnSeries(Γ, (HahnSeries(Γ', R))) \\to HahnSeries(\\text{Lex}(\\text{Prod } Γ Γ'), R)$ with $\\text{coeff}(g) = \\text{coeff}(\\text{coeff } x\\ g.1)\\ g.2$$$
Lean4
/-- Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product. -/
def ofIterate [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) : HahnSeries (Γ ×ₗ Γ') R
where
coeff := fun g => coeff (coeff x g.1) g.2
isPWO_support' := by
refine Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_
· refine Set.IsPWO.mono x.isPWO_support' ?_
simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]
exact fun _ ↦ ne_zero_of_coeff_ne_zero
· exact fun a => by simpa [Function.mem_support, ne_eq] using (x.coeff a).isPWO_support'
