English
For any finite set s, a permutation f maps s to s iff its inverse maps s to s.
Русский
Для любого конечного множества s перестановка f переводит s в s тогда и только тогда, когда её обратная отображает s в s.
LaTeX
$$$\\forall {f : \\mathrm{Perm}(\\alpha)} {s : \\mathrm{Set}\\; \\alpha} [\\mathrm{Finite}~s],\\; \\mathrm{MapsTo}(f^{-1}, s, s) \\Leftrightarrow \\mathrm{MapsTo}(f, s, s)$$$
Lean4
theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α} (hy : y ∈ s) :
f⁻¹ y ∈ s :=
by
have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
(fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
obtain ⟨y2, hy2, heq⟩ := h0 y hy
convert hy2
rw [heq]
simp only [inv_apply_self]
