isUniformEmbedding_coeFn — Mathlib

English

The coercion map is a uniform embedding from UniformConvergenceCLM to UniformOnFun.

Русский

Коэрцинное отображение является равномерно встраиваемым из UniformConvergenceCLM в UniformOnFun.

LaTeX

$$$\\operatorname{IsUniformEmbedding}\\left( \\alpha := \\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}) , \\; \\mathrm{UniformOnFun.ofFun}\\,𝔖 \\circ \\mathrm{DFunLike.coe} \\right)$$$

Lean4

theorem isUniformEmbedding_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  ⟨isUniformInducing_coeFn .., DFunLike.coe_injective⟩

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