closure_isCycle — Mathlib

English

In the symmetric group on a finite set β, the subgroup generated by all cycles is the entire group; equivalently, the closure of the set {σ ∈ Perm β | IsCycle σ} is the whole Perm β.

Русский

В симметрической группе на конечном множестве β подгруппа, порождаемая всеми циклами, есть вся группа; иначе говоря, замыкание множества {σ ∈ Perm β | IsCycle σ} равно всей Perm β.

LaTeX

$$$\mathrm{closure}\{\sigma \in \mathrm{Perm}(β) : \mathrm{IsCycle}(σ)\} = \mathrm{Perm}(β)$$$

Lean4

theorem closure_isCycle : closure {σ : Perm β | IsCycle σ} = ⊤ := by
  classical
  cases nonempty_fintype β
  exact top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

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