English
If E is a locally convex space over 𝕜 and X is a topological space, then the space C(X, E) is a locally convex space over 𝕜.
Русский
Если E — локально выпуклое пространство над полем 𝕜, а X — топологическое пространство, то пространство непрерывных отображений C(X, E) тоже локально выпукло над 𝕜.
LaTeX
$$\\(LocallyConvexSpace\\, 𝕜\\, C(X, E)\\) holds under the hypotheses: E locally convex, X topological, ContinuousAdd/ContinuousConstSMul as appropriate.$$
Lean4
instance instLocallyConvexSpace {X 𝕜 E : Type*} [TopologicalSpace X] [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E]
[Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] :
LocallyConvexSpace 𝕜 C(X, E) :=
.ofBasisZero _ _ _ _ (LocallyConvexSpace.convex_basis_zero 𝕜 E).nhds_continuousMapConst <|
by
rintro ⟨K, U⟩ ⟨hK, hU₀, hUc⟩ f hf g hg a b ha hb hab x hx
exact hUc (hf hx) (hg hx) ha hb hab
