Theorems · Theorem · functional analysis

ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} {l : Filter α} {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F},
  Filter.Tendsto f l (nhds A) ↔
    ∀ (x : E) (y : F), Filter.Tendsto (fun a => inner 𝕜 y ((f a) x)) l (nhds (inner 𝕜 y (A x)))

The defining property of the weak operator topology: a function f tends to A : E →WOT[𝕜] F along filter l iff ⟪y, (f a) x⟫ tends to ⟪y, A x⟫ along the same filter.

Defined in

Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeAddCommGroupTopologicalSpaceModuleNormedAddCommGroupInnerProductSpaceCompleteSpace