Theorems · Theorem · functional analysis

WeakBilin.continuous_of_continuous_eval_re

∀ {α : Type u_4} {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [inst : TopologicalSpace α] [inst_1 : RCLike 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {g : α → WeakBilin B}, (∀ (y : F), Continuous fun a => RCLike.re ((B (g a)) y)) → Continuous g

A map into WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) over 𝕜 (with RCLike 𝕜) is continuous if the real parts of all the evaluation maps a ↦ B (g a) y are continuous for each y : F.

Defined in

Mathlib.Analysis.Normed.Module.WeakDual

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRCLikeAddCommGroupModuleAddCommGroupModule