closure_isSwap — Mathlib

English

The set of all swap-permutations on a finite α generates the whole symmetric group; the closure of swaps is the whole group.

Русский

Множество транспозиционных перестановок на конечном α порождает всю симметрическую группу; их замыкание равно всей группе.

LaTeX

$$$ [Finite\\ α] \\Rightarrow \\overline{\\{\\sigma : Perm(α) \\mid \\sigma \\text{ is swap} \\}} = \\top $$$

Lean4

theorem closure_isSwap [Finite α] : Subgroup.closure {σ : Perm α | IsSwap σ} = ⊤ :=
  Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_isSwap

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