disjoint_iff_disjoint_support — Mathlib

English

Two permutations f and g are disjoint if and only if their supports are disjoint as sets.

Русский

Две перестановки f и g располагются независимо (Disjoint) тогда и только тогда, когда их опоры как множества не пересекаются.

LaTeX

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

Lean4

theorem disjoint_iff_disjoint_support : Disjoint f g ↔ _root_.Disjoint f.support g.support := by
  simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, imp_iff_not_or]

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