English
Combining an equivalence between two subtypes with an equivalence between their complements yields a permutation of the ambient type.
Русский
Совмещение эквиваленций между подтипами и между их дополнениями порождает перестановку над всем множеством.
LaTeX
$$$ \\text{SubtypeCongr}:\\; \\text{Equiv.Perm } \\varepsilon = \\text{permCongr }(\\,\\textsum) \\,.$$$
Lean4
/-- Combines an `Equiv` between two subtypes with an `Equiv` between their complements to form a
permutation. -/
def subtypeCongr {α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] (e : { x // p x } ≃ { x // q x })
(f : { x // ¬p x } ≃ { x // ¬q x }) : Perm α :=
(sumCompl p).symm.trans ((sumCongr e f).trans (sumCompl q))
