disjoint_iff — Mathlib

English

For finsupps f,g over a canonically ordered additive structure, Disjoint f g is equivalent to Disjoint f.support g.support.

Русский

Для функций FinSupp f,g над канонически упорядоченным аддитивным набором, Disjoint f g эквивалентно Disjoint supp(f) supp(g).

LaTeX

$$$\\operatorname{Disjoint}(f,g) \\iff \\operatorname{Disjoint}(f.\\operatorname{support}, g.\\operatorname{support})$$$

Lean4

nonrec theorem disjoint_iff {f g : ι →₀ α} : Disjoint f g ↔ Disjoint f.support g.support := by
  classical
  rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty, Finsupp.support_inf]
  rfl

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