case h.h
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
x✝ : α
a✝ : β
⊢ ↑(curry' f x✝) a✝ = ↑((comp f ∘ coev β α) x✝) a✝
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
⊢ curry' f = comp f ∘ coev β α
ext
no goals
case h.h
α : Type u_2
β : Type u_1
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
x✝ : α
a✝ : β
⊢ ↑(curry' f x✝) a✝ = ↑((comp f ∘ coev β α) x✝) a✝
rfl