English
If f is a uniform embedding, then postcomposition by f is a uniform embedding on the uniform convergence spaces.
Русский
Если f — равномерно вложение, то пост-композиция на пространствах равномерной конвергенции является равномерным вложением.
LaTeX
$$$$ \text{If } f \text{ is a uniform embedding, then } (f \circ \cdot): (α \to^{u} γ) \to (α \to^{u} β) \text{ is a uniform embedding}. $$$$
Lean4
/-- Post-composition by a uniform embedding is
a uniform embedding for the uniform structures of uniform convergence.
More precisely, if `f : γ → β` is a uniform embedding,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is a uniform embedding. -/
protected theorem postcomp_isUniformEmbedding [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) :
IsUniformEmbedding (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β)
where
toIsUniformInducing := UniformFun.postcomp_isUniformInducing hf.isUniformInducing
injective _ _ H := funext fun _ ↦ hf.injective (congrFun H _)
