English
If c and d are cycles of g, then d preserves the support of c; equivalently, for all x, d x ∈ support(c) iff x ∈ support(c).
Русский
Если c и d — циклы g, то d сохраняет опору цикла c; то есть для любого x выполняется: d x ∈ опора(c) ⇔ x ∈ опора(c).
LaTeX
$$$\forall g,d,c : \mathrm{Perm}(\alpha),\; hc : c \in g.\mathrm{cycleFactorsFinset},\; hd : d \in g.\mathrm{cycleFactorsFinset} \;\Rightarrow \; \forall x:\alpha,\; d x \in c.\mathrm{support} \leftrightarrow x \in c.\mathrm{support}$$$
Lean4
/-- If `c` and `d` are cycles of `g`, then `d` stabilizes the support of `c` -/
theorem mem_support_cycle_of_cycle {g d c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (hd : d ∈ g.cycleFactorsFinset) :
∀ x : α, d x ∈ c.support ↔ x ∈ c.support := by
intro x
simp only [mem_support, not_iff_not]
by_cases h : c = d
· rw [← h, EmbeddingLike.apply_eq_iff_eq]
·
rw [← Perm.mul_apply, Commute.eq (cycleFactorsFinset_mem_commute g hc hd h), mul_apply,
EmbeddingLike.apply_eq_iff_eq]
