English
Let Γ, Γ' be partially ordered sets and V an additive module over R with compatible order structure. For x ∈ HahnSeries(Γ, R) and y ∈ HahnModule(Γ', R, V), the support of the element obtained from x and y via the canonical map is contained in the vertical sum of the supports; i.e. Supp((of R)^{-1}(x · y)) ⊆ Supp(x) +_v Supp((of R)^{-1} y).
Русский
Пусть Γ, Γ' частично упорядочены, V — модуль над R с совместимой упорядоченностью. Для x ∈ HahnSeries(Γ, R) и y ∈ HahnModule(Γ', R, V) множество опор элемента, образованного из x и y через каноническое отображение, содержится в вертикальной сумме опор Supp(x) и Supp((of R)^{-1} y).
LaTeX
$$$\\operatorname{Supp}((\\mathrm{of}\\, R)^{-1}(x \\cdot y)) \\subseteq \\operatorname{Supp}(x) \\,+_{v}\\ \\operatorname{Supp}((\\mathrm{of}\\, R)^{-1} y).$$$
Lean4
theorem support_smul_subset_vadd_support [MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R}
{y : HahnModule Γ' R V} : ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support := by
exact support_smul_subset_vadd_support'
