isUniformEmbedding_comp — Mathlib

English

The composition of a uniform embedding g with the inducing structure yields a uniform embedding of the composition map, i.e., if g is uniformly embedding, then the map x ↦ g ∘ x is uniformly embeddable.

Русский

Если g — равномерно внедряющее отображение, то композиция x ↦ g ∘ x также является равномерно внедряемой.

LaTeX

$$$\text{IsUniformEmbedding } (g \circ -)$$$

Lean4

theorem isUniformEmbedding_comp {Y : Type*} [UniformSpace Y] [Zero Y] (g : C(Y, R)₀) (hg : IsUniformEmbedding g) :
    IsUniformEmbedding (g.comp · : C(X, Y)₀ → C(X, R)₀) :=
  isUniformEmbedding_toContinuousMap.of_comp_iff.mp <|
    ContinuousMap.isUniformEmbedding_comp g.toContinuousMap hg |>.comp isUniformEmbedding_toContinuousMap

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