disjoint_support — Mathlib

English

If f and g are disjoint permutations, then the support of their product equals the union of their supports: supp(fg) = supp(f) ∪ supp(g).

Русский

Если f и g — взаимно независимые перестановки, то опора произведения fg равна объединению их опор: supp(fg) = supp(f) ∪ supp(g).

LaTeX

$$$\operatorname{supp}(f g) = \operatorname{supp}(f) \cup \operatorname{supp}(g)$, when f and g are disjoint.$$

Lean4

theorem disjoint_support (h : Disjoint f g) : _root_.Disjoint f.support g.support :=
  disjoint_iff_disjoint_support.1 h

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