disjoint_prod_perm — Mathlib

English

If l1 and l2 are lists of permutations that are permutation-equivalent and l1 is a pairwise-disjoint list, then l1.prod = l2.prod.

Русский

Если список перестановок l1 эквивалентен по перестановке списку l2 и элементы l1 попарно несовместны, то произведения совпадают.

LaTeX

$$$\forall \{l_1,l_2:\text{List}(\operatorname{Perm}(\alpha))\},\ l_1 \sim l_2\;\land\; l_1\text{.Pairwise Disjoint} \Rightarrow l_1.\mathrm{prod} = l_2.\mathrm{prod}$$$

Lean4

theorem disjoint_prod_perm {l₁ l₂ : List (Perm α)} (hl : l₁.Pairwise Disjoint) (hp : l₁ ~ l₂) : l₁.prod = l₂.prod :=
  hp.prod_eq' <| hl.imp Disjoint.commute

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