X✝ : Type ?u.327951
Y : Type ?u.327954
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
x y z : X✝
ι✝ : Type ?u.327969
γ✝ : Path x y
X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ 0 ≤ 1
X✝ : Type ?u.327951
Y : Type ?u.327954
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
x y z : X✝
ι✝ : Type ?u.327969
γ✝ : Path x y
X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ Continuous ↿fun t => extend (γ t)
refine' h.comp (continuous_id.prod_map continuous_projIcc)
no goals
X✝ : Type ?u.327951
Y : Type ?u.327954
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
x y z : X✝
ι✝ : Type ?u.327969
γ✝ : Path x y
X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ 0 ≤ 1
exact zero_le_one