English
The support of f - g is contained in the support of f: any coordinate where f - g is nonzero must come from a nonzero f-coordinate.
Русский
Поддержка f − g ⊆ поддержка f: координата, где (f − g) не равна нулю, должна происходить из не нулевой координаты f.
LaTeX
$$$ (f - g).\mathrm{support} \subseteq f.\mathrm{support} $$$
Lean4
theorem support_tsub : (f - g).support ⊆ f.support := by
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, Ne, coe_tsub, Pi.sub_apply, not_imp_not,
zero_le, imp_true_iff]