disjoint_iff — Mathlib

English

Two dfinsupps are disjoint iff their supports are disjoint.

Русский

Два dfinsupp попарно несоприкасаются тогда и только тогда, когда их поддержки не пересекаются.

LaTeX

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

Lean4

nonrec theorem disjoint_iff : Disjoint f g ↔ Disjoint f.support g.support :=
  by
  rw [disjoint_iff, disjoint_iff, DFinsupp.bot_eq_zero, ← DFinsupp.support_eq_empty, DFinsupp.support_inf]
  rfl

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