English
If h₁ describes how p is preserved by a permutation f and h₂ ensures that points outside the subtype stay outside, then the subtype-permutation induced by extending f to α agrees with f on the subtype, i.e. extending and then restricting recovers f.
Русский
Если h₁ описывает, как подтип сохраняется перестановкой f, а h₂ гарантирует, что точки вне подтипа остаются вне подтипа, то перестановка на подтип, полученная как продолжение f, совпадает с f на подтипе.
LaTeX
$$$ \\operatorname{subtypePerm}(\\operatorname{ofSubtype} f)\_{?} = f, \\text{ i.e. } \\operatorname{subtypePerm}(\\operatorname{ofSubtype} f)\\! (\\operatorname{ofSubtype\\_apply\\_mem}\\! f) = f$$$
Lean4
theorem ofSubtype_subtypePerm {f : Perm α} (h₁ : ∀ x, p (f x) ↔ p x) (h₂ : ∀ x, f x ≠ x → p x) :
ofSubtype (subtypePerm f h₁) = f :=
Equiv.ext fun x => by
by_cases hx : p x
· exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx
· rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk, Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
exact not_not.mp fun h => hx (h₂ x (Ne.symm h))
