case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
z✝ : G
⊢ Continuous fun g => g • ↑z✝
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
x : G ⧸ Γ
⊢ Continuous fun g => g • x
induction x using QuotientGroup.induction_on
no goals
case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
z✝ : G
⊢ Continuous fun g => g • ↑z✝
exact continuous_quotient_mk'.comp (continuous_mul_right _)