English
For equicontinuous F on a compact X, IsUniformInducing of UniformFun.ofFun ∘ F is equivalent to IsUniformInducing F.
Русский
Для равномерно ограниченного F на компактном X изоморфность UniformFun.ofFun ∘ F равна IsUniformInducing F.
LaTeX
$$$ [UniformSpace ι] [CompactSpace X] (F\_eqcont : Equicontinuous F) : \ IsUniformInducing (UniformFun.ofFun ∘ F) \\leftrightarrow IsUniformInducing F $$$
Lean4
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the topologies of uniform convergence and pointwise convergence induce
the same topology on `ι`.
In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.
This is a consequence of `Equicontinuous.comap_uniformFun_eq`, stated in terms of `IsInducing`
for convenience. -/
theorem inducing_uniformFun_iff_pi [TopologicalSpace ι] [CompactSpace X] (F_eqcont : Equicontinuous F) :
IsInducing (UniformFun.ofFun ∘ F) ↔ IsInducing F :=
by
rw [isInducing_iff, isInducing_iff]
change
(_ = (UniformFun.uniformSpace X α |>.comap F |>.toTopologicalSpace)) ↔
(_ = (Pi.uniformSpace _ |>.comap F |>.toTopologicalSpace))
rw [F_eqcont.comap_uniformFun_eq]
