case a.h
X : Type u_1
Y✝ : Type ?u.306794
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y✝
x y z : X
ι : Type ?u.306809
γ✝ γ : Path x y
Y : Type u_2
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
x✝ : ↑I
⊢ ↑(map (map γ hf) hg) x✝ = ↑(map γ (_ : Continuous (g ∘ f))) x✝
X : Type u_1
Y✝ : Type ?u.306794
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y✝
x y z : X
ι : Type ?u.306809
γ✝ γ : Path x y
Y : Type u_2
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
⊢ map (map γ hf) hg = map γ (_ : Continuous (g ∘ f))
ext
no goals
case a.h
X : Type u_1
Y✝ : Type ?u.306794
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y✝
x y z : X
ι : Type ?u.306809
γ✝ γ : Path x y
Y : Type u_2
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
x✝ : ↑I
⊢ ↑(map (map γ hf) hg) x✝ = ↑(map γ (_ : Continuous (g ∘ f))) x✝
rfl