ext_inner — Mathlib

English

In the weak operator topology, a net f converges to A if and only if, for all x,y, the inner products ⟪y, (f a) x⟫ converge to ⟪y, A x⟫ along the same net.

Русский

В слабой операторной топологии сеть функций сходится к A тогда и только тогда, если для всех x,y верны сходящиеся значения ⟪y, (f a) x⟫ → ⟪y, A x⟫ по той же сети.

LaTeX

$$$ \\text{Tendsto}(f,l,\\mathcal{N}A) \\iff \\forall x,y,\n \\text{Tendsto}(a \\mapsto \\langle y, (f(a)) x \\rangle_\\mathbb{K})\,l\\, (\\mathcal{N}\\langle y, A x \\rangle_\\mathbb{K})$$$

Lean4

@[ext]
theorem ext_inner {A B : E →WOT[𝕜] F} (h : ∀ x y, ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜) : A = B :=
  by
  rw [ext_iff]
  exact fun x => ext_inner_left 𝕜 fun y => h x y

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