Theorems · Theorem · functional analysis

PointwiseConvergenceCLM.continuous_of_continuous_eval

∀ {α : Type u_1} [inst : TopologicalSpace α] {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst_1 : NormedField 𝕜₁]
  [inst_2 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [inst_3 : AddCommGroup E]
  [inst_4 : TopologicalSpace E] [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜₁ E] [inst_9 : Module 𝕜₂ F] {g : α → E →SLₚₜ[σ] F},
  (∀ (x : E), Continuous fun x_1 => (g x_1) x) → Continuous g

A map to E →SLₚₜ[σ] F is continuous if for every x : E the evaluation g · x is continuous.

Defined in

Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedFieldNormedFieldAddCommGroupTopologicalSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleModule