ContinuousLinearMapWOT — Mathlib

English

The weak operator topology is defined by taking the underlying set E →L[𝕜] F and equipping it with the weak operator topology: i.e., the weak operator copy of continuous linear maps from E to F.

Русский

Слабая операторная топология определяется на множества E →L[𝕜] F, наделяя его копией слабой операторной топологии соответствующее множество непрерывных линейных отображений из E в F.

LaTeX

$$$\\mathrm{ContinuousLinearMapWOT}_{𝕜}(E,F) := E \\to_L[𝕜] F$$$

Lean4

/-- The type copy of `E →L[𝕜] F` endowed with the weak operator topology, denoted as
`E →WOT[𝕜] F`. -/
@[irreducible]
def ContinuousLinearMapWOT (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜] [AddCommGroup E] [TopologicalSpace E]
    [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] :=
  E →L[𝕜] F

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