isUniformEmbedding_toUniformOnFun

English

There exists a uniform embedding from the space of continuous linear maps E →SL[σ] F into a space of uniformly controlled functions, via UniformOnFun.

Русский

Существует равномерная вложенность пространства непрерывных линейных отображений в пространство функций с равномерной связью, через UniformOnFun.

LaTeX

$$IsUniformEmbedding (fun f => UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f)$$

Lean4

theorem isUniformEmbedding_toUniformOnFun [UniformSpace F] [IsUniformAddGroup F] :
    IsUniformEmbedding fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f :=
  UniformConvergenceCLM.isUniformEmbedding_coeFn ..

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