Theorems · Theorem · functional analysis

UniformFun.continuousSMul_induced_of_range_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] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E]
  [inst_9 : FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom),
  Topology.IsInducing (⇑UniformFun.ofFun ∘ ⇑φ) →
    (∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) → ContinuousSMul 𝕜 H

Let E be a topological vector space over a normed field 𝕜, let α be any type. Let H be a submodule of α →ᵤ E such that the range of each f ∈ H is von Neumann bounded. Then H is a topological vector space over 𝕜, i.e., the pointwise scalar multiplication is continuous in both variables. For convenience we require that H is a vector space over 𝕜 with a topology induced by UniformFun.ofFun ∘ φ, where φ : H →ₗ[𝕜] (α → E).

Defined in

Mathlib.Topology.Algebra.Module.UniformConvergence

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldAddCommGroupModuleAddCommGroupModuleTopologicalSpaceUniformSpaceIsUniformAddGroupContinuousSMulFunLikeLinearMapClass