isCycle_cycleOf — Mathlib

English

If f x ≠ x then IsCycle (cycleOf f x).

Русский

Если f x ≠ x, то IsCycle (cycleOf f x).

LaTeX

$$isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x)$$

Lean4

theorem isCycle_cycleOf (f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) : IsCycle (cycleOf f x) :=
  have : cycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
  (isCycle_iff_sameCycle this).2
    @fun y =>
      ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
        if hxy : SameCycle f x y then
          let ⟨i, hi⟩ := hxy
          ⟨i, by rw [cycleOf_zpow_apply_self, hi]⟩
        else by
          rw [cycleOf_apply_of_not_sameCycle hxy] at h
          exact (h rfl).elim⟩

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