closure_of_isSwap_of_isPretransitive

English

If a symmetric generating set of swaps yields a pretransitive action, then the generated subgroup is the entire permutation group.

Русский

Если симметричный набор транспозиций генерирует предпереносимую точность действия, то получившаяся подгруппа порождает всю группу перестановок.

LaTeX

$$$\\text{closure}(S) = \\top$$$

Lean4

/-- A transitive permutation group generated by transpositions must be the whole symmetric group -/
theorem closure_of_isSwap_of_isPretransitive [Finite α] {S : Set (Perm α)} (hS : ∀ σ ∈ S, σ.IsSwap)
    [MulAction.IsPretransitive (Subgroup.closure S) α] : Subgroup.closure S = ⊤ := by
  simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite]

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