support_add_subset — Mathlib

English

For Hahn series x and y, the support of their sum is contained in the union of their supports: supp(x+y) ⊆ supp(x) ∪ supp(y).

Русский

Для рядов Хана x и y поддержка их суммы содержится в объединении поддержек: supp(x+y) ⊆ supp(x) ∪ supp(y).

LaTeX

$$$$ \operatorname{supp}(x+y) \subseteq \operatorname{supp}(x) \cup \operatorname{supp}(y). $$$$

Lean4

theorem support_add_subset {x y : HahnSeries Γ R} : support (x + y) ⊆ support x ∪ support y := fun a ha =>
  by
  rw [mem_support, coeff_add] at ha
  rw [Set.mem_union, mem_support, mem_support]
  contrapose! ha
  rw [ha.1, ha.2, add_zero]

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