instUniformSpace

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

The space E →WOT 𝕜 F is equipped with a uniform structure induced by inducingFn.

Русский

Пространство E →WOT 𝕜 F оснащено униформной структурой, полученной через отображение inducingFn.

LaTeX

$$instUniformSpace : UniformSpace (E →WOT[𝕜] F)$$

Lean4

instance instUniformSpace : UniformSpace (E →WOT[𝕜] F) :=
  .comap (inducingFn 𝕜 E F) inferInstance

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

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

Разделы

Аффилиация

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