English
If the complement of fixedBy α g is contained in s, then s ∈ fixedBy (Set α) g; i.e., g cannot move a point of s outside s.
Русский
Если комплемент фиксированных точек относительно g содержится в s, то s фиксируется действием g, то есть g не переносит точку из s за пределы s.
LaTeX
$$$ (fixedBy α g)^{c} \subseteq s \Rightarrow s \in fixedBy(Set α) g $$$
Lean4
/-- If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`. -/
@[to_additive /-- If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`. -/
]
theorem set_mem_fixedBy_of_movedBy_subset {s : Set α} {g : G} (s_subset : (fixedBy α g)ᶜ ⊆ s) : s ∈ fixedBy (Set α) g :=
by
rw [← fixedBy_inv]
ext a
rw [Set.mem_inv_smul_set_iff]
by_cases a ∈ fixedBy α g
case pos a_fixed => rw [a_fixed]
case neg a_moved =>
constructor <;> (intro; apply s_subset)
· exact a_moved
· rwa [Set.mem_compl_iff, smul_mem_fixedBy_iff_mem_fixedBy]
