isEmbedding_coeFn — Mathlib

English

Alternative statement that the embedding property holds for the coercion map between the same spaces.

Русский

Альтернативное утверждение: вложение сохраняется для отображения приведения между теми же пространствами.

LaTeX

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

Lean4

theorem isEmbedding_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsEmbedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  IsUniformEmbedding.isEmbedding (isUniformEmbedding_coeFn _ _ _)

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