subtypePerm_on_cycleFactorsFinset

English

A permutation restricted to the cycle support equals the corresponding cycle factor on that support.

Русский

У перестановки, ограниченной опорой цикла, совпадает её цикл-фактор на этой опоре.

LaTeX

$$$\forall {g,c} (hc : c ∈ g.\mathrm{cycleFactorsFinset}) : g.\mathrm{subtypePerm}(\mathrm{mem_cycleFactorsFinset_support hc}) = c.\mathrm{subtypePermOfSupport}$$$

Lean4

/-- A permutation restricted to the support of a cycle factor is that cycle factor -/
theorem subtypePerm_on_cycleFactorsFinset [DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
    g.subtypePerm (mem_cycleFactorsFinset_support hc) = c.subtypePermOfSupport :=
  by
  ext ⟨x, hx⟩
  simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
  exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm

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