English
If f is a uniform inducing map, then the postcomposition map is a uniform inducing map between the corresponding 𝔖-convergence spaces.
Русский
Если f — равномерно порождающее отображение, то отображение по пост-композиции порождает равномерность между соответствующими пространствами 𝔖-конвергенций.
LaTeX
$$IsUniformInducing f → IsUniformInducing (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖).$$
Lean4
/-- Post-composition by a uniform inducing is a uniform inducing for the
uniform structures of `𝔖`-convergence.
More precisely, if `f : γ → β` is a uniform inducing, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform inducing. -/
theorem postcomp_isUniformInducing [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) :
IsUniformInducing (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by
-- This is a direct consequence of `UniformOnFun.comap_eq`
constructor
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
change comap (Prod.map (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)) _ = _
rw [← uniformity_comap] at hf ⊢
congr
rw [← UniformSpace.ext hf, UniformOnFun.comap_eq]
rfl
