def QuotientGroup.continuousMulEquiv {G : Type u_1} {H : Type u_2} [Group G] (N : Subgroup G) [N.Normal] [Group H] (M : Subgroup H) [M.Normal] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ* H) (h : Subgroup.map (↑e) N = M) : G ⧸ N ≃ₜ* H ⧸ M

def QuotientAddGroup.continuousAddEquiv {G : Type u_1} {H : Type u_2} [AddGroup G] (N : AddSubgroup G) [N.Normal] [AddGroup H] (M : AddSubgroup H) [M.Normal] [TopologicalSpace G] [TopologicalSpace H] (e : G ≃ₜ+ H) (h : AddSubgroup.map (↑e) N = M) : G ⧸ N ≃ₜ+ H ⧸ M

theorem QuotientGroup.isOpenQuotientMap_rightrel_mk {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) : IsOpenQuotientMap (Quot.mk ⇑(rightRel H))