mem_cycleFactorsFinset_support — Mathlib

English

If c ∈ g.cycleFactorsFinset, then applying g does not change the membership of elements in c.support: g a ∈ c.support iff a ∈ c.support.

Русский

Если c ∈ cycleFactorsFinset g, то применение g не меняет принадлежность элемента к опоре c: g a ∈ c.support ↔ a ∈ c.support.

LaTeX

$$$\forall g,c : \mathrm{Perm}(\alpha),\; (hc : c \in g.\mathrm{cycleFactorsFinset})\;\forall a:\alpha,\; g a \in c.\mathrm{support} \iff a \in c.\mathrm{support}$$$

Lean4

/-- If a permutation is a cycle of `g`, then its support is invariant under `g`. -/
theorem mem_cycleFactorsFinset_support {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (a : α) :
    g a ∈ c.support ↔ a ∈ c.support :=
  mem_support_iff_of_commute (self_mem_cycle_factors_commute hc).symm a

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