instModule — Mathlib

English

There exists a natural linear equivalence between the usual space of continuous linear maps E →L[𝕜] F and the weak operator topology copy E →WOT[𝕜] F, given by the identity map.

Русский

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

LaTeX

$$$(E \\toL[𝕜] F) \\cong_{𝕜} (E \\toWOT[𝕜] F)$$$

Lean4

instance instModule [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : Module 𝕜 (E →WOT[𝕜] F) :=
  inferInstanceAs <| Module 𝕜 (E →L[𝕜] F)

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