English
If hf : f.IsCycleOn s, then the subtype permutation on s is a cycle on Set.univ, i.e., the entire ambient universe is a single cycle when viewed through the subtype.
Русский
Если f — цикл на s, то перестановка на подтипе isCycleOn для Set.univ; вся вселенная образует единый цикл в таком виде.
LaTeX
$$$\mathrm{IsCycleOn}(f,s) \Rightarrow \mathrm{IsCycleOn}\bigl( f|_s, \mathrm{Set.univ} \bigr)$$$
Lean4
/-- Note that the identity is a cycle on any subsingleton set, but not a cycle. -/
protected theorem subtypePerm (hf : f.IsCycleOn s) :
(f.subtypePerm fun _ => hf.apply_mem_iff : Perm s).IsCycleOn _root_.Set.univ :=
by
obtain hs | hs := s.subsingleton_or_nontrivial
· haveI := hs.coe_sort
exact isCycleOn_of_subsingleton _ _
convert (hf.isCycle_subtypePerm hs).isCycleOn
rw [eq_comm, Set.eq_univ_iff_forall]
exact fun x =>
ne_of_apply_ne ((↑) : s → α)
(hf.apply_ne hs x.2)
-- TODO: Theory of order of an element under an action
