sameCycle_iff_cycleOf_eq_of_mem_support

English

If x and y are in the support of g, then x and y are in the same cycle of g iff the cycle_of x equals cycle_of y.

Русский

Если x и y лежат в поддержке g, то x и y принадлежат одному и тому же циклу g тогда и только тогда, когда cycleOf x = cycleOf y.

LaTeX

$$$x \\\\in g\\\\.support \\\\land y \\\\in g\\\\.support \\\\Rightarrow (g.SameCycle x y) \\\\iff g\\\\.cycleOf x = g\\\\.cycleOf y$$$

Lean4

theorem sameCycle_iff_cycleOf_eq_of_mem_support [DecidableEq α] [Fintype α] {g : Perm α} {x y : α} (hx : x ∈ g.support)
    (hy : y ∈ g.support) : g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y :=
  by
  refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩
  rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h, mem_support_cycleOf_iff' (mem_support.mp hy)]

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