support_zpowers_of_mem_cycleFactorsFinset_le

English

If v is a z-power of a cycle factor c of g, then its support lies inside g's support.

Русский

Если v — z-образ цикла c фактора g, то опора v лежит в опоре g.

LaTeX

$$$v : Subgroup.zpowers(c) \Rightarrow (v:Perm\alpha).\mathrm{support} \subseteq g.support$$$

Lean4

theorem support_zpowers_of_mem_cycleFactorsFinset_le {g : Perm α} {c : g.cycleFactorsFinset}
    (v : Subgroup.zpowers (c : Perm α)) : (v : Perm α).support ≤ g.support :=
  by
  obtain ⟨m, hm⟩ := v.prop
  simp only [← hm]
  exact le_trans (support_zpow_le _ _) (mem_cycleFactorsFinset_support_le c.prop)

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