instCompleteSpace — Mathlib

English

Restriction of scalars 𝕜' from 𝕜 to 𝕜' yields a uniform embedding of ContinuousMultilinearMap 𝕜 E F into ContinuousMultilinearMap 𝕜' E F.

Русский

Сужение скаляров 𝕜' из 𝕜 даёт равномерное вложение ContinuousMultilinearMap 𝕜 E F в ContinuousMultilinearMap 𝕜' E F.

LaTeX

$$UniformEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')$$

Lean4

instance instCompleteSpace [∀ i, IsTopologicalAddGroup (E i)] [SequentialSpace (Π i, E i)] :
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F) :=
  completeSpace <| .of_seq fun _u x hux ↦ (hux.isVonNBounded_range 𝕜).insert x

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