English
Let l be a filter and f: α → E →WOT[𝕜] F, A: E →WOT[𝕜] F. Then f tends to A along l in the weak operator topology iff for every x ∈ E and every continuous linear functional y on F, the scalars y(f(a)(x)) converge to y(Ax) along l.
Русский
Пусть l — фильтр, f: α → E →WOT[𝕜] F, A: E →WOT[𝕜] F. Тогда f tends to A по l в слабой операторной топологии тогда и только тогда, когда для каждого x ∈ E и каждого непрерывного линейного функционала y на F выполнится, что y(f(a)(x)) сходится к y(Ax) по l.
LaTeX
$$$\\\\operatorname{Tendsto} f\\\\, l\\\\, \\\\mathcal{N} A \\\\iff \\\\forall x \in E, \, \forall y \in F^*, \\\\operatorname{Tendsto} (a \mapsto y(f(a)(x))) \\, l \\, \mathcal{N} (y(Ax)).$$$
Lean4
/-- 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. -/
theorem tendsto_iff_forall_dual_apply_tendsto {α : Type*} {l : Filter α} {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} :
Tendsto f l (𝓝 A) ↔ ∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))) := by
simp [isInducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]
