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