τ : Type u_2
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_1
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (curry (uncurry ϕ.toFun) t)
τ : Type u_2
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_1
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (toFun ϕ t)
rw [←curry_uncurry ϕ.toFun]
case h
τ : Type u_2
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_1
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (uncurry ϕ.toFun)
τ : Type u_2
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_1
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (curry (uncurry ϕ.toFun) t)
apply continuous_curry
no goals
case h
τ : Type u_2
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_1
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (uncurry ϕ.toFun)
exact ϕ.cont'