English
For a permutation f, f is a cycle if and only if there exists a subset s of α that is nontrivial, f is a cycle on s, and every non-fixed point x lies in s. In symbols: f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ x, ¬IsFixedPt f x → x ∈ s.
Русский
Для перестановки f верно: f образует цикл тогда и только тогда, когда существует множество s ⊆ α, которое не тождественно пустое; f образует цикл на s, и любой нефиксируемый элемент принадлежит s.
LaTeX
$$$f\text{ is a cycle } \iff \exists s: \mathrm{Set}(\alpha), \ s \text{ is nontrivial } \land \mathrm{IsCycleOn}(f,s) \land \forall x, \neg \mathrm{IsFixedPt}(f,x) \rightarrow x \in s$$$
Lean4
/-- This lemma demonstrates the relation between `Equiv.Perm.IsCycle` and `Equiv.Perm.IsCycleOn`
in non-degenerate cases. -/
theorem isCycle_iff_exists_isCycleOn :
f.IsCycle ↔ ∃ s : Set α, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x⦄, ¬IsFixedPt f x → x ∈ s :=
by
refine ⟨fun hf => ⟨{x | f x ≠ x}, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
· obtain ⟨a, ha⟩ := hf
exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
· rintro ⟨s, hs, hf, hsf⟩
obtain ⟨a, ha⟩ := hs.nonempty
exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩
