isEmbedding_toUniformOnFun — Mathlib

English

The map toUniformOnFun is an embedding from ContinuousMultilinearMap into the UniformOnFun space.

Русский

Отображение toUniformOnFun является вложением (эмбеддингом) ContinuousMultilinearMap в пространство UniformOnFun.

LaTeX

$$IsEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F))$$

Lean4

theorem isEmbedding_toUniformOnFun :
    IsEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) :=
  isUniformEmbedding_toUniformOnFun.isEmbedding

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