isUniformEmbedding_toUniformOnFun

English

The map toUniformOnFun is uniform-inducing from ContinuousMultilinearMap to its UniformOnFun representation.

Русский

Отображение toUniformOnFun является равномерно-индуктивным от ContinuousMultilinearMap к его представлению UniformOnFun.

LaTeX

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

Lean4

theorem isUniformEmbedding_toUniformOnFun : IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) :=
  ⟨isUniformInducing_toUniformOnFun, DFunLike.coe_injective⟩

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