UniformOnFun.continuousSMul_submodule_of_image_bounded
theorem UniformOnFun.continuousSMul_submodule_of_image_bounded :
โ (๐ : Type u_1) (ฮฑ : Type u_2) (E : Type u_3) [inst : NormedField ๐] [inst_1 : AddCommGroup E]
[inst_2 : Module ๐ E] [inst_3 : UniformSpace E] [inst_4 : UniformAddGroup E] [inst_5 : ContinuousSMul ๐ E]
{๐ : Set (Set ฮฑ)} (H : Submodule ๐ (UniformOnFun ฮฑ E ๐)),
(โ u โ H, โ s โ ๐, Bornology.IsVonNBounded ๐ (u '' s)) โ ContinuousSMul ๐ โฅH
The theorem `UniformOnFun.continuousSMul_submodule_of_image_bounded` states that given a topological vector space `E`, a set `๐` of subsets of `ฮฑ`, and a submodule `H` of functions from `ฮฑ` to `E` that converges uniformly on the given set `๐`, if the image of any subset `S` in `๐` under any function `u` from `H` is von Neumann bounded (i.e., every neighborhood of zero absorbs this image), then the submodule `H`, when equipped with the topology of `๐`-convergence, forms a topological vector space (TVS). In other words, the scalar multiplication operation in this submodule is continuous. The comment also suggests that if you are having difficulty using this theorem, consider using the previous one instead.
More concisely: Given a topological vector space E, a set ๐ of subsets of ฮฑ, and a submodule H of functions from ฮฑ to E that uniformly converges on ๐ and maps ๐ into von Neumann bounded sets, H is a topological vector space with respect to the ๐-convergence topology.
|
UniformOnFun.continuousSMul_induced_of_image_bounded
theorem UniformOnFun.continuousSMul_induced_of_image_bounded :
โ (๐ : Type u_1) (ฮฑ : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [inst : NormedField ๐]
[inst_1 : AddCommGroup H] [inst_2 : Module ๐ H] [inst_3 : AddCommGroup E] [inst_4 : Module ๐ E]
[inst_5 : TopologicalSpace H] [inst_6 : UniformSpace E] [inst_7 : UniformAddGroup E] [inst_8 : ContinuousSMul ๐ E]
{๐ : Set (Set ฮฑ)} [inst_9 : FunLike hom H (ฮฑ โ E)] [inst_10 : LinearMapClass hom ๐ H (ฮฑ โ E)] (ฯ : hom),
Inducing (โ(UniformOnFun.ofFun ๐) โ โฯ) โ
(โ (u : H), โ s โ ๐, Bornology.IsVonNBounded ๐ (ฯ u '' s)) โ ContinuousSMul ๐ H
This theorem states that given a topological vector space `E`, a set `๐` of subsets of some type `ฮฑ`, and a vector space `H` (not necessarily a submodule of the function space from `ฮฑ` to `E` with `๐`-convergence), along with a linear mapping `ฯ` from `H` to the function space, if the image of any subset `S` in `๐` under any vector `u` in `H` is von Neumann bounded (i.e. every neighborhood of 0 absorbs the image set), then `H`, when equipped with the topology of `๐`-convergence, becomes a topological vector space. The theorem provides a more usable condition in terms of an arbitrary vector space `H` and a linear inducing to the function space, rather than needing `H` to be a submodule of the function space.
More concisely: Given a topological vector space `E`, a set `๐` of subsets of some type `ฮฑ`, a vector space `H` with a linear mapping `ฯ` to the function space from `ฮฑ` to `E`, if the image of each `๐`-neighborhood of `0` in `H` is von Neumann bounded, then `H` with `๐`-convergence becomes a topological vector space.
|