instT3Space — Mathlib

English

The weak operator topology space of linear maps E → WOT F is a T3 (regular) space provided F has a separating dual.

Русский

Пространство слабой операторной топологии отображений E → WOT F является T3 (регулярным), если у слоя F есть разделяющий дуал.

LaTeX

$$$\text{T3Space} (E \toWOT[\mathbb{K}] F)$$$

Lean4

instance instT3Space [SeparatingDual 𝕜 F] : T3Space (E →WOT[𝕜] F) :=
  isEmbedding_inducingFn.t3Space

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