English
If f is cycle-on s and s is nontrivial, then the induced permutation on s, viewed as a permutation of the ambient universe, is a cycle on Set.univ.
Русский
Если f является циклом на s и s композиционно ненулево, тогда индуцированная перестановка на s, рассматриваемая как перестановка над всей вселенной, является циклом на Set.univ.
LaTeX
$$$\mathrm{IsCycleOn}(f,s) \land s \text{ Nontrivial } \Rightarrow \mathrm{IsCycleOn}\bigl( f_{|s} : \mathrm{Perm}(s), \mathrm{Set.univ} \bigr)$$$
Lean4
/-- Note that the identity satisfies `IsCycleOn` for any subsingleton set, but not `IsCycle`. -/
theorem isCycle_subtypePerm (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
(f.subtypePerm fun _ => hf.apply_mem_iff : Perm s).IsCycle :=
by
obtain ⟨a, ha⟩ := hs.nonempty
exact ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ => (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩
