isUniformEmbedding_comp — Mathlib

English

If g is a uniform embedding, then the postcomposition by g is a uniform embedding on C-spaces: f ↦ g ∘ f.

Русский

Если g — униформное вложение, то предпосечение по g образует униформное вложение на пространствах функций.

LaTeX

$$$hg : IsUniformEmbedding g \Rightarrow IsUniformEmbedding (\,f\mapsto g\circ f\,)$$$

Lean4

theorem isUniformEmbedding_comp (g : C(β, δ)) (hg : IsUniformEmbedding g) :
    IsUniformEmbedding (ContinuousMap.comp g : C(α, β) → C(α, δ)) :=
  isUniformEmbedding_toUniformOnFunIsCompact.of_comp_iff.mp <|
    UniformOnFun.postcomp_isUniformEmbedding hg |>.comp isUniformEmbedding_toUniformOnFunIsCompact

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