X✝ : Type ?u.469179
Y : Type ?u.469182
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.469197
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous fun x => (t, x)
⊢ Continuous ↿(truncate γ t)
X✝ : Type ?u.469179
Y : Type ?u.469182
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.469197
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous ↿(truncate γ t)
have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by continuity
no goals
X✝ : Type ?u.469179
Y : Type ?u.469182
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.469197
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous fun x => (t, x)
⊢ Continuous ↿(truncate γ t)
exact γ.truncate_continuous_family.comp key
no goals
X✝ : Type ?u.469179
Y : Type ?u.469182
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.469197
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous fun x => (t, x)
continuity