English
Given a directed family of index sets 𝔖 and a nonempty collection of sets, the space of uniformly convergent continuous linear maps UniformConvergenceCLM σ F 𝔖 is locally convex.
Русский
Условиe: задано направленное семейство индексов 𝔖; пространство нулевых характеристик непрерывных линейных отображений UniformConvergenceCLM σ F 𝔖 локально выпукло.
LaTeX
$$$\text{LocallyConvexSpace}(R,\,\mathrm{UniformConvergenceCLM}(\sigma, F, \mathbb{S}))$$$
Lean4
theorem locallyConvexSpace (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖) :=
by
apply
LocallyConvexSpace.ofBasisZero _ _ _ _
(UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂ (LocallyConvexSpace.convex_basis_zero R F)) _
rintro ⟨S, V⟩ ⟨_, _, hVconvex⟩ f hf g hg a b ha hb hab x hx
exact hVconvex (hf x hx) (hg x hx) ha hb hab
