instTopologicalSpace — Mathlib

English

Reiterates the correspondence between UniformOnFun and continuous multilinear maps via toUniformOnFun.

Русский

Повторяет соответствие между UniformOnFun и непрерывными мультилинеарными отображениями через toUniformOnFun.

LaTeX

$$То же, что и предыдущий пункт: диапазон toUniformOnFun описывается как множество UniformOnFun, порождаемых непрерывными мультилинеарными отображениями.$$

Lean4

instance instTopologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] :
    TopologicalSpace (ContinuousMultilinearMap 𝕜 E F) :=
  .induced toUniformOnFun <| @UniformOnFun.topologicalSpace _ _ (IsTopologicalAddGroup.toUniformSpace F) _

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