X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.347696
γ : Path x y
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous fun t => trans (f t) (g t)
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.347696
γ : Path x y
f : Y → Path x y
g : Y → Path y z
⊢ Continuous f → Continuous g → Continuous fun t => trans (f t) (g t)
intro hf hg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.347696
γ : Path x y
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous ↿fun t => trans (f t) (g t)
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.347696
γ : Path x y
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous fun t => trans (f t) (g t)
apply continuous_uncurry_iff.mp
no goals
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.347696
γ : Path x y
f : Y → Path x y
g : Y → Path y z
hf : Continuous f
hg : Continuous g
⊢ Continuous ↿fun t => trans (f t) (g t)
exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)