continuous_toWOT — Mathlib

English

Reiterates that the weak operator topology space is an UniformAddGroup.

Русский

Повторное утверждение: слабое операторное пространство — униформная группа по сложению.

LaTeX

$$instance instIsUniformAddGroup : IsUniformAddGroup (E →WOT[𝕜] F)$$

Lean4

/-- The weak operator topology is coarser than the bounded convergence topology, i.e. the inclusion
map is continuous. -/
@[continuity, fun_prop]
theorem continuous_toWOT : Continuous (ContinuousLinearMap.toWOT 𝕜 E F) :=
  ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y ↦ y.cont.comp <| continuous_eval_const x

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