isCycleOn_of_subsingleton — Mathlib

English

If the ambient type is a subsingleton, then any permutation is a cycle on any subset.

Русский

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

LaTeX

$$$\\forall \\alpha, \\text{ Subsingleton}(\\alpha) \\Rightarrow \\forall f:\\mathrm{Perm}(\\alpha), \\forall s \\subseteq \\alpha, f.IsCycleOn s.$$$

Lean4

theorem isCycleOn_of_subsingleton [Subsingleton α] (f : Perm α) (s : Set α) : f.IsCycleOn s :=
  ⟨s.bijOn_of_subsingleton _, fun x _ y _ => (Subsingleton.elim x y).sameCycle _⟩

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