isPWO_iUnion_support_prod_mul — Mathlib

English

The union of supports of products is well-founded if the two unions are well-founded.

Русский

Объединение опор произведений хорошо упорядочено, если оба объединения хорошо упорядочены.

LaTeX

$$$ isPWO_iUnion\_support\_prod\_mul \; hs ht : (\bigcup a, (s a).support).IsPWO \Rightarrow (\bigcup b, (t b).support).IsPWO \Rightarrow (\bigcup (a,b), ((s a.1) * (t a.2)).support).IsPWO $$$

Lean4

theorem isPWO_iUnion_support_prod_mul {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ R}
    (hs : (⋃ a, (s a).support).IsPWO) (ht : (⋃ b, (t b).support).IsPWO) :
    (⋃ (a : α × β), ((fun a ↦ ((s a.1) * (t a.2))) a).support).IsPWO :=
  isPWO_iUnion_support_prod_smul hs ht

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