English
If g and h commute, then the set fixed by g is fixed by h: (fixedBy α g) ∈ fixedBy (Set α) h, i.e., for all x, h • x ∈ fixedBy α g iff x ∈ fixedBy α g.
Русский
Если g и h commute, то множество фиксированных точек g фиксируется относительно h: (fixedBy α g) ∈ fixedBy (Set α) h, т.е. для каждого x: h • x ∈ fixedBy α g ⇔ x ∈ fixedBy α g.
LaTeX
$$$ (fixedBy(α, g)) \in fixedBy(Set α, h) $$$
Lean4
/-- If `s ⊆ fixedBy α g`, then `g • s = s`, which means that `s ∈ fixedBy (Set α) g`.
Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a
weaker statement (it allows for points `x ∈ s` for which `g • x ≠ x` and `g • x ∈ s`).
-/
@[to_additive /-- If `s ⊆ fixedBy α g`, then `g +ᵥ s = s`, which means that `s ∈ fixedBy (Set α) g`.
Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a
weaker statement (it allows for points `x ∈ s` for which `g +ᵥ x ≠ x` and `g +ᵥ x ∈ s`). -/
]
theorem set_mem_fixedBy_of_subset_fixedBy {s : Set α} {g : G} (s_ss_fixedBy : s ⊆ fixedBy α g) :
s ∈ fixedBy (Set α) g := by
rw [← fixedBy_inv]
ext x
rw [Set.mem_inv_smul_set_iff]
refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩
rw [← fixedBy_inv] at s_ss_fixedBy
rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs
