mono — Mathlib

English

If f and g are disjoint and x and y have supports contained in f and g respectively, then x and y are disjoint.

Русский

Если f и g — взаимно непересекающиеся перестановки, и x, y имеют поддержки, вложенные в поддержки f и g соответственно, то x и y несовпадаемы по опоре.

LaTeX

$$Theorem: If Disjoint f g and x.support ≤ f.support and y.support ≤ g.support, then Disjoint x y.$$

Lean4

theorem mono {x y : Perm α} (h : Disjoint f g) (hf : x.support ≤ f.support) (hg : y.support ≤ g.support) :
    Disjoint x y := by
  rw [disjoint_iff_disjoint_support] at h ⊢
  exact h.mono hf hg

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