English
Assume Γ, Γ' are linear orders and the usual additive structure interacts well with the WithTop construction. Then, under a compatibility condition h that respects the WithTop extension, the orderTop of the scaled element x via y dominates the sum of the orderTop of x and the orderTop of y after applying the canonical embedding; i.e., x.orderTop +_v (of R)^{-1} y.orderTop ≤ (of R)^{-1}(x · y).orderTop.
Русский
Пусть Γ, Γ' образуют линейные порядки, дополнение WithTop ведёт себя как положено. При условии совместимости h, сохраняющего WithTop, порядокTop произведения x и y не меньше суммы orderTop(x) и orderTop(y) после соответствующего отображения: x.orderTop +_v (of R)^{-1} y.orderTop ≤ (of R)^{-1}(x · y).orderTop.
LaTeX
$$$\\forall x \\in HahnSeries(Γ,R), y \\in HahnModule(Γ',R,V), (h:\\forall γ,γ', γ+_v γ'=(γ:WithTop Γ)+_v(γ':WithTop Γ')) \\; x.orderTop +_v ((\\mathrm{of}\\, R).symm y).orderTop \\leq ((\\mathrm{of}\\, R).symm (x \\cdot y)).orderTop.$$$
Lean4
theorem orderTop_vAdd_le_orderTop_smul {Γ Γ'} [LinearOrder Γ] [LinearOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ']
[MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R} [VAdd (WithTop Γ) (WithTop Γ')] {y : HahnModule Γ' R V}
(h : ∀ (γ : Γ) (γ' : Γ'), γ +ᵥ γ' = (γ : WithTop Γ) +ᵥ (γ' : WithTop Γ')) :
x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop :=
by
by_cases hx : x = 0; · simp_all
by_cases hy : y = 0; · simp_all
have hhy : ((of R).symm y) ≠ 0 := hy
rw [HahnSeries.orderTop_of_ne_zero hx, HahnSeries.orderTop_of_ne_zero hhy, ← h, ← Set.IsWF.min_vadd]
by_cases hxy : (of R).symm (x • y) = 0
· rw [hxy, HahnSeries.orderTop_zero]
exact OrderTop.le_top (α := WithTop Γ') _
· rw [HahnSeries.orderTop_of_ne_zero hxy, WithTop.coe_le_coe]
exact Set.IsWF.min_le_min_of_subset support_smul_subset_vadd_support
