case h.h
X : Type u_4
𝕜 : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ ↑(↑↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ =
    ↑(↑(ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝
X : Type u_4
𝕜 : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
⊢ ↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g
ext f
no goals
case h.h
X : Type u_4
𝕜 : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ ↑(↑↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ =
    ↑(↑(ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝
rfl