instTopologicalSpace — Mathlib

English

The weak operator topology on E →L F is the coarsest topology making all evaluations (A ↦ y(Ax)) continuous, i.e., the induced topological structure from inducingFn to the product topology.

Русский

Слабая операторная топология на E →L F — это самая грубая топология, делающая все отображения A ↦ y(Ax) непрерывными, то есть индукцированная структура над произведением.

LaTeX

$$$\\text{TopologicalSpace}(E \\toWOT[𝕜] F) = \\text{induced}(\\text{inducingFn}, \\Pi\\text{-top})$$$

Lean4

/-- The weak operator topology is the coarsest topology such that `fun A => y (A x)` is
continuous for all `x, y`. -/
instance instTopologicalSpace : TopologicalSpace (E →WOT[𝕜] F) :=
  .induced (inducingFn _ _ _) Pi.topologicalSpace

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