isCycleOn — Mathlib

English

Let f be a permutation of a type α which forms a single cycle. Then f is a cycle when restricted to the set of moving points { x ∈ α : f(x) ≠ x }. In symbols: If IsCycle(f), then IsCycleOn(f, { x ∈ α | f(x) ≠ x }).

Русский

Пусть f — перестановка множества α, образующая один цикл. Тогда restriction of f на множество движущихся точек { x ∈ α | f(x) ≠ x } образует цикл на α. Формально: Если IsCycle(f), то IsCycleOn(f, { x ∈ α | f(x) ≠ x }).

LaTeX

$$$\mathrm{IsCycle}(f) \Rightarrow \mathrm{IsCycleOn}\bigl(f, \{x \in \alpha \mid f(x) \neq x\}\bigr)$$$

Lean4

protected theorem isCycleOn (hf : f.IsCycle) : f.IsCycleOn {x | f x ≠ x} :=
  ⟨f.bijOn fun _ => f.apply_eq_iff_eq.not, fun _ ha _ => hf.sameCycle ha⟩

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