English
If f is a uniform inducing, then the postcomposition map is uniform inducing between the corresponding 𝔖-convergence spaces.
Русский
Если f — равномерно индуцирующее отображение, то отображение по пост-композиции между соответствующими 𝔖-конвергенциями является равномерно индуцирующим.
LaTeX
$$IsUniformInducing f → IsUniformInducing (Function.comp (UniformOnFun.ofFun 𝔖) (Function.comp (fun x => Function.comp f x) (UniformOnFun.toFun 𝔖))).$$
Lean4
/-- If `𝔖` covers `α`, the natural map `UniformOnFun.toFun` from `α →ᵤ[𝔖] β` to `α → β` is
uniformly continuous.
In other words, if `𝔖` covers `α`, then the uniform structure of `𝔖`-convergence is finer than
that of pointwise convergence. -/
protected theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) : UniformContinuous (toFun 𝔖 : (α →ᵤ[𝔖] β) → α → β) :=
by
rw [uniformContinuous_pi]
exact uniformContinuous_eval h
