cycleOf_mem_cycleFactorsFinset_iff

English

The cycle containing x is a cycle factor of f exactly when x belongs to the support of f.

Русский

Цикл, содержащий x, является фактором цикла f тогда и только тогда, когда x принадлежит опоре f.

LaTeX

$$$cycleOf(f,x) \in cycleFactorsFinset(f) \iff x \in f.support$$$

Lean4

theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} : cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support :=
  by
  rw [mem_cycleFactorsFinset_iff]
  constructor
  · rintro ⟨hc, _⟩
    contrapose! hc
    rw [notMem_support, ← cycleOf_eq_one_iff] at hc
    simp [hc]
  · intro hx
    refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩
    intro y hy
    rw [mem_support] at hy
    rw [cycleOf_apply]
    split_ifs with H
    · rfl
    · rw [cycleOf_apply_of_not_sameCycle H] at hy
      contradiction

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