instContinuousNeg

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMapWOT.instContinuousNeg

English

Negation is a continuous operation on E →WOT 𝕜 F.

Русский

Отрицание непрерывно на пространстве слабой операторной топологии.

LaTeX

$$ContinuousNeg (E →WOT[𝕜] F)$$

Lean4

instance instContinuousNeg : ContinuousNeg (E →WOT[𝕜] F) :=
  .induced (inducingFn 𝕜 E F)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru