English
There is a MonoidHom from Perm({a | p a}) × Perm({a | ¬p a}) to Perm α, given by toFun(f,g) = Perm.subtypeCongr(f,g).
Русский
Существует моноид-гомоморфизм от Perm({a | p a}) × Perm({a | ¬p a}) в Perm α, заданный отображением toFun(f,g) = Perm.subtypeCongr(f,g).
LaTeX
$$$$ \mathrm{subtypeCongrHom}_p:\mathrm{Perm}({a\mid p a}) \times \mathrm{Perm}({a\mid \lnot p a}) \to^* \mathrm{Perm}(\alpha), \quad \text{toFun}(f,g)=\mathrm{Perm.subtypeCongr}(f,g). $$$$
Lean4
/-- `Equiv.Perm.subtypeCongr` as a `MonoidHom`. -/
@[simps]
def subtypeCongrHom (p : α → Prop) [DecidablePred p] : Perm { a // p a } × Perm { a // ¬p a } →* Perm α
where
toFun pair := Perm.subtypeCongr pair.fst pair.snd
map_one' := Perm.subtypeCongr.refl
map_mul' _ _ := (Perm.subtypeCongr.trans _ _ _ _).symm
