le_nhds_iff_forall_inner_apply_le_nhds

English

A net is below the nhds of A in the weak-operator topology if and only if every inner-product projection along any vector family stays below the corresponding target

Русский

Набор сетей удовлетворяет взаимному включению в окрестность A в слабой топологии операторов тогда и только тогда каждый проекционный элемент через внутреннее произведение не превышает целевой предел.

LaTeX

$$$ \\ell \\le \\mathcal{N}A \\iff \\forall x,y,\\ \\ell.map (T \\mapsto \\langle y, T x \\rangle) \\le \\mathcal{N}\\langle y, A x\\rangle$$$

Lean4

theorem le_nhds_iff_forall_inner_apply_le_nhds [CompleteSpace F] {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} :
    l ≤ 𝓝 A ↔ ∀ x y, l.map (fun T => ⟪y, T x⟫_𝕜) ≤ 𝓝 (⟪y, A x⟫_𝕜) :=
  tendsto_iff_forall_inner_apply_tendsto (f := id)

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