support_tsub — Mathlib

English

For any f1,f2 : ι →₀ α, the support of their truncated difference is contained in the support of f1.

Русский

Для любых f1,f2 : ι →₀ α опора разности f1 - f2 вложена в опору f1.

LaTeX

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

Lean4

theorem support_tsub {f1 f2 : ι →₀ α} : (f1 - f2).support ⊆ f1.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]

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