English
For an equicontinuous family on a compact X, the uniform structures of uniform convergence and pointwise convergence pull back to the same on the index set.
Русский
Пусть F равносильно ограничено на компактном X; тогда проекция структур сходится обратно одинаково для равномерной и покоенной сходимости.
LaTeX
$$$ (F_eqcont: Equicontinuous F) \to (UniformFun.uniformSpace X α).comap F = (Pi.uniformSpace _).comap F $$$
Lean4
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the uniform structures of uniform convergence and pointwise
convergence induce the same uniform structure on `ι`.
In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.
This is a version of `Equicontinuous.comap_uniformFun_eq` stated in terms of `IsUniformInducing`
for convenience. -/
theorem isUniformInducing_uniformFun_iff_pi [UniformSpace ι] [CompactSpace X] (F_eqcont : Equicontinuous F) :
IsUniformInducing (UniformFun.ofFun ∘ F) ↔ IsUniformInducing F :=
by
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace, ← F_eqcont.comap_uniformFun_eq]
rfl
