F✝ : Type ?u.11079
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ ↑(↑(extend F) t) x = ↑F (1, x)
F✝ : Type ?u.11079
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ ↑(↑(extend F) t) x = ↑f₁ x
rw [← F.apply_one]
no goals
F✝ : Type ?u.11079
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ ↑(↑(extend F) t) x = ↑F (1, x)
exact ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x