α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous Inv.inv
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
⊢ Continuous Inv.inv
letI := g.toTopologicalSpace
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : TopologicalGroup α
⊢ Continuous Inv.inv
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous Inv.inv
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 Inv.inv
exact continuous_inv