perm_inv_mapsTo_of_mapsTo — Mathlib

English

If a permutation maps a finite subset into itself, then its inverse also maps that subset into itself.

Русский

Если перестановка отображает конечный поднабор в сам поднабор, то её обратная тоже отображает в сам поднабор.

LaTeX

$$$\\forall {f : \\mathrm{Perm}(\\alpha)} {s : \\mathrm{Set}\\; \\alpha} [\\mathrm{Finite}~s], (f\\;\\text{MapsTo } s\\; s) \\Rightarrow (f^{-1}\\;\\text{MapsTo } s\\; s)$$$

Lean4

theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) : Set.MapsTo (f⁻¹ :) s s :=
  by
  cases nonempty_fintype s
  exact fun x hx =>
    Set.mem_toFinset.mp <|
      perm_inv_on_of_perm_on_finset (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
        (Set.mem_toFinset.mpr hx)

Похожие утверждения