instDecidableRelSameCycle — Mathlib

English

On a finite set, the relation of being in the same cycle for a fixed permutation is decidable.

Русский

На конечном множестве отношение нахождения в одном цикле фиксированной перестановки разрешимо вычислением.

LaTeX

$$$[DecidableRel\\\\ (SameCycle \\\\mathrm{f})] \\\\Rightarrow \\\\text{for all } x,y: \\\\mathrm{SameCycle}\\\\(f,x,y)\\\\text{ is decidable}$$$

Lean4

instance instDecidableRelSameCycle [DecidableEq α] [Fintype α] (f : Perm α) : DecidableRel (SameCycle f) := fun x y =>
  decidable_of_iff (y ∈ List.iterate f x (Fintype.card α)) <|
    by
    simp only [List.mem_iterate, iterate_eq_pow, eq_comm (a := y)]
    constructor
    · rintro ⟨n, _, hn⟩
      exact ⟨n, hn⟩
    · intro hxy
      by_cases hx : x ∈ f.support
      case pos =>
        -- we can't invoke the aux lemmas above without obtaining the decidable instance we are
                -- already building; but now we've left the data, so we can do this non-constructively
                -- without sacrificing computability.

        let _inst (f : Perm α) : DecidableRel (SameCycle f) := Classical.decRel _
        rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
        refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩
      case neg =>
        haveI : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

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