English
The induced permutation sends a subtype element x to (f x) together with the preserved predicate
Русский
Индуцированная перестановка отправляет элемент-подтип x в f x с сохранением предиката.
LaTeX
$$$\\forall {f : \\mathrm{Perm}(\\alpha)} {p : \\alpha \\to \\mathrm{Prop}} [\\mathrm{Finite} {x : \\alpha \\mid p x}] (h : \\forall x, p x \\to p (f x)) (x : \\{ x : \\alpha \\mid p x\\}) \\,\\mathrm{subtypePermOfFintype}\, h (x) = \\langle f x, h x x.2 \\rangle$$$
Lean4
/-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
`Equiv.Perm.subtypePerm`. -/
abbrev subtypePermOfFintype (f : Perm α) {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x)) :
Perm { x // p x } :=
f.subtypePerm fun x => ⟨fun h₂ => f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂, h x⟩
