support_smul_subset_vadd_support'

English

The support of x•y is contained in the v-addition of supports: supp((x)•(y)) ⊆ supp(x) +ᵥ supp(y).

Русский

Поддержка x•y ⊆ поддержка x +ᵥ поддержка y.

LaTeX

$$supp(x \\cdot y) \\subseteq supp(x) +^∨ supp(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
  apply Set.Subset.trans (fun x hx => _) support_vaddAntidiagonal_subset_vadd
  · exact x.isPWO_support
  · exact y.isPWO_support
  intro x hx
  contrapose! hx
  simp only [Set.mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
  simp [hx, coeff_smul]

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