support_inf — Mathlib

English

For finsupps f,g, the support of their infimum equals the intersection of their supports: (f ⊓ g).support = f.support ∩ g.support.

Русский

Для функций FinSupp f,g опора их наименьшего (inf) равна пересечению опор: supp(f ⊓ g) = supp(f) ∩ supp(g).

LaTeX

$$$ (f \\inf g).\\operatorname{support} = f.\\operatorname{support} \\cap g.\\operatorname{support} $$$

Lean4

@[simp]
theorem support_inf [DecidableEq ι] (f g : ι →₀ α) : (f ⊓ g).support = f.support ∩ g.support :=
  by
  ext
  simp only [inf_apply, mem_support_iff, Ne, Finset.mem_inter]
  simp only [← nonpos_iff_eq_zero, min_le_iff, not_or]

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