English
The union of supports of two summable families is well-founded, hence their bilinear combination has well-founded support.
Русский
Объединение опор двух суммируемых семейств является хорошо упорядоченным; следовательно, их билинейное сочетание имеет хорошо упорядоченную опору.
LaTeX
$$$ (\bigcup_{a} (s a).\mathrm{support}).IsPWO \wedge (\bigcup_{b} (t b).\mathrm{support}).IsPWO \Longrightarrow (\bigcup_{(a,b)} ((s a.1) \cdot (t a.2)).\mathrm{support}).IsPWO $$$
Lean4
theorem isPWO_iUnion_support_prod_smul {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ' V}
(hs : (⋃ a, (s a).support).IsPWO) (ht : (⋃ b, (t b).support).IsPWO) :
(⋃ (a : α × β), ((fun a ↦ (of R).symm ((s a.1) • (of R) (t a.2))) a).support).IsPWO :=
by
apply (hs.vadd ht).mono
have hsupp :
∀ ab : α × β,
support ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab) ⊆ (s ab.1).support +ᵥ (t ab.2).support :=
by
intro ab
refine
Set.Subset.trans (fun x hx => ?_)
(support_vaddAntidiagonal_subset_vadd (hs := (s ab.1).isPWO_support) (ht := (t ab.2).isPWO_support))
contrapose! hx
simp only [Set.mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
refine Set.Subset.trans (Set.iUnion_mono fun a => (hsupp a)) ?_
simp_all only [Set.iUnion_subset_iff, Prod.forall]
exact fun a b =>
Set.vadd_subset_vadd (Set.subset_iUnion_of_subset a fun x y ↦ y) (Set.subset_iUnion_of_subset b fun x y ↦ y)
