perm_inv_mapsTo_iff_mapsTo — Mathlib

English

The inverse mapsTo relation is equivalent to the mapsTo relation for the original permutation.

Русский

Отношение обратной отображения mapsTo эквивалентно отношению mapsTo для исходной перестановки.

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

@[simp]
theorem perm_inv_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] : Set.MapsTo (f⁻¹ :) s s ↔ Set.MapsTo f s s :=
  ⟨perm_inv_mapsTo_of_mapsTo f⁻¹, perm_inv_mapsTo_of_mapsTo f⟩

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