English
Same as item 6: the subgroup generated by all cycles equals the full symmetric group on a finite set.
Русский
То же, что и пункт 6: подгруппа, порождаемая всеми циклами, равна всей симметрической группе над конечным множеством.
LaTeX
$$closure {σ : Perm β | IsCycle σ} = ⊤$$
Lean4
protected theorem extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
IsCycle g → IsCycle (g.extendDomain f) := by
rintro ⟨a, ha, ha'⟩
refine ⟨f a, ?_, fun b hb => ?_⟩
· rw [extendDomain_apply_image]
exact Subtype.coe_injective.ne (f.injective.ne ha)
have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
rw [apply_symm_apply, Subtype.coe_mk]
rw [h] at hb ⊢
simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
exact (ha' hb).extendDomain
