isCycleOn_support_of_mem_cycleFactorsFinset

English

As above, establishing the equivalence with membership in the support.

Русский

Как выше, эквивалентность между равенством cycleOf и принадлежностью опоре.

LaTeX

$$Same as 124016$$

Lean4

theorem isCycleOn_support_of_mem_cycleFactorsFinset {g c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset) :
    IsCycleOn g c.support :=
  by
  obtain ⟨x, hx⟩ := IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp hc).1
  rw [cycle_is_cycleOf hx hc]
  exact isCycleOn_support_cycleOf g x

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