mem_fixedPoints_or_exists_zpow_eq

English

For any a ∈ g.Basis and x ∈ α with hx ∈ cycle factors, x and g.cycleOf x lie in the same cycle of g.

Русский

Для a ∈ g.Basis и x ∈ α, если x относится к циклу, то x и g.cycleOf x лежат в одной и той же цикл‑обозначенной цепи поколения g.

LaTeX

$$∀ x, hx ∈ g.cycleFactorsFinset → g.SameCycle (g.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset.coe a ⟨g.cycleOf x, hx⟩) x$$

Lean4

theorem mem_fixedPoints_or_exists_zpow_eq (x : α) :
    x ∈ Function.fixedPoints g ∨ ∃ (c : g.cycleFactorsFinset) (_ : x ∈ c.val.support) (m : ℤ), (g ^ m) (a c) = x :=
  by
  rw [Classical.or_iff_not_imp_left]
  intro hx
  rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support, ← cycleOf_mem_cycleFactorsFinset_iff] at hx
  refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩
  rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]
  simp [SameCycle.rfl, hx, and_self]

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