The space of continuous maps is a locally convex space

In this file we prove that the space of continuous maps from a topological space to a locally convex topological vector space is a locally convex topological vector space.

instance ContinuousMap.instLocallyConvexSpace {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [TopologicalSpace X] [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] : LocallyConvexSpace 𝕜 C(X, E)