English
If the set of non-fixed points of a permutation σ is contained in s, then σ maps s onto itself: σ''s = s.
Русский
Если множество неподвижных точек перестановки σ ограничено множеством s, то σ отображает s на себя: σ''s = s.
LaTeX
$$$\\{a : \\alpha \\mid \\sigma(a) \\neq a\\} \\subseteq s \\Rightarrow \\sigma''s = s$$$
Lean4
/-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
-/
theorem image_perm {s : Set α} {σ : Equiv.Perm α} (hs : {a : α | σ a ≠ a} ⊆ s) : σ '' s = s :=
by
ext i
obtain hi | hi := eq_or_ne (σ i) i
· refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
rintro ⟨j, hj, h⟩
rwa [σ.injective (hi.trans h.symm)]
· refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
grind
