tendsto_iff_forall_eval_tendsto_topDualPairing

English

Convergence in the weak space is characterized by convergence of all evaluations against every vector in the underlying space.

Русский

Сходимость в слабом пространстве характеризуется сходимостью по всем оцениваниям против каждого вектора во внутреннем пространстве.

LaTeX

$$$\\forall y,\\; \\mathrm{Tendsto} (i \\mapsto \\ topDualPairing 𝕜 E (f i) y)\\ l\\ (nhds (topDualPairing 𝕜 E x y))$ при $Tendsto f l (nhds x)$$$

Lean4

theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α → WeakDual 𝕜 E} {x : WeakDual 𝕜 E} :
    Tendsto f l (𝓝 x) ↔ ∀ y, Tendsto (fun i => topDualPairing 𝕜 E (f i) y) l (𝓝 (topDualPairing 𝕜 E x y)) :=
  WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective

Похожие утверждения