cycleFactorsFinset_pairwise_disjoint

English

Let f be a permutation of a finite type. Then the cycle factors of f are pairwise disjoint.

Русский

Пусть f — перестановка на конечном множестве. Тогда цикловые факторы f образуют пару взаимоисключающих элементов.

LaTeX

$$$\forall p,q\\in cycleFactorsFinset(f),\; p\neq q \Rightarrow p \perp q$$$

Lean4

theorem cycleFactorsFinset_pairwise_disjoint : (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint :=
  (cycleFactorsFinset_eq_finset.mp rfl).2.choose

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