α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous fun p => p.fst * p.snd
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
⊢ Continuous fun p => p.fst * p.snd
letI := g.toTopologicalSpace
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : TopologicalGroup α
⊢ Continuous fun p => p.fst * p.snd
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous fun p => p.fst * p.snd
haveI := g.toTopologicalGroup
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : TopologicalGroup α
⊢ Continuous fun p => p.fst * p.snd
exact continuous_mul