support_tsub — Mathlib

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]

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