isPWO_iUnion_support_powers — Mathlib

English

If a Hahn series x has nonnegative order, then the union over all powers of its support is well-founded with respect to the order: (⋃n (x^n).support).IsPWO.

Русский

Если порядок Ган_series x невозрастающий, то объединение опор всех степеней x является хорошо упорядоченным по порядку: (⋃_n (x^n).support).IsPWO.

LaTeX

$$$\bigcup_{n\in\mathbb{N}} (x^n).\operatorname{support} \; \text{IsPWO}.$$$

Lean4

theorem isPWO_iUnion_support_powers [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R]
    {x : HahnSeries Γ R} (hx : 0 ≤ x.order) : (⋃ n : ℕ, (x ^ n).support).IsPWO :=
  (x.isPWO_support'.addSubmonoid_closure fun _ hg =>
        le_trans hx (order_le_of_coeff_ne_zero (Function.mem_support.mp hg))).mono
    (Set.iUnion_subset fun n => support_pow_subset_closure x n)

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