English
For a conj-action k acting on Perm α and a permutation g, a ∈ α lies in the support of k^{-1}·g if and only if k acts by conjugation on a and moves a into the support of g.
Русский
При действии сопряжения k на Perm α элемент a принадлежит опоре k^{-1}·g тогда и только тогда, когда сопряжение переводит a в опору g.
LaTeX
$$theorem mem_conj_support (k : ConjAct (Perm α)) (g : Perm α) (a : α) : a ∈ (k • g).support ↔ ConjAct.ofConjAct k⁻¹ a ∈ g.support$$
Lean4
/-- `a : α` belongs to the support of `k • g` iff
`k⁻¹ * a` belongs to the support of `g` -/
theorem mem_conj_support (k : ConjAct (Perm α)) (g : Perm α) (a : α) :
a ∈ (k • g).support ↔ ConjAct.ofConjAct k⁻¹ a ∈ g.support :=
by
simp only [mem_support, ConjAct.smul_def, not_iff_not, coe_mul, Function.comp_apply, ConjAct.ofConjAct_inv]
apply Equiv.apply_eq_iff_eq_symm_apply
