subset_support_tsub — Mathlib

English

The difference of supports satisfies Supp(f1) \\ Supp(f2) ⊆ Supp(f1 - f2).

Русский

Разности множеств опор удовлетворяет Supp(f1) \\ Supp(f2) ⊆ Supp(f1 - f2).

LaTeX

$$$\\operatorname{Supp}(f_1) \\setminus \\operatorname{Supp}(f_2) \\subseteq \\operatorname{Supp}(f_1 - f_2)$$$

Lean4

theorem subset_support_tsub [DecidableEq ι] {f1 f2 : ι →₀ α} : f1.support \ f2.support ⊆ (f1 - f2).support := by
  simp +contextual [subset_iff]

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