mem_support_iff_mem_support_of_mem_cycleFactorsFinset

English

A permutation p belongs to the cycle factors of f iff p is a cycle and acts like f on its support.

Русский

Перестановка p принадлежит цикловым факторам f тогда и только тогда, когда p — цикл и на своей опоре действует как f.

LaTeX

$$$\forall {f,p}: p \in cycleFactorsFinset(f) \iff p.IsCycle \land \forall a \in p.support, p(a)=f(a)$$$

Lean4

theorem mem_support_iff_mem_support_of_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support :=
  by
  constructor
  · intro h
    use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h
    rw [mem_support_cycleOf_iff]
    exact ⟨SameCycle.refl g x, h⟩
  · rintro ⟨c, hc, hx⟩
    exact mem_cycleFactorsFinset_support_le hc hx

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