English
Let X be a space, 𝔖 a covering of X by compact subsets, α a uniform space, and F: ι → X → α equicontinuous on every K ∈ 𝔖. Then the topology induced by uniform convergence on 𝔖 coincides with the topology induced by pointwise convergence on ⋃₀𝔖, when viewed through the corresponding restriction map. In particular, the two notions of convergence yield the same topology on ι.
Русский
Пусть X — пространство, 𝔖 — покрытие X компактными частями, α — униформное пространство, и F: ι → X → α равномерно непрерывно на каждом K ∈ 𝔖. Тогда топологии, индуцированные униформной сходимостью на 𝔖 и покомплексной сходимостью по ⋃₀𝔖, совпадают через соответствующую схему ограничения, т.е. двух топологий на ι совпадают.
LaTeX
$$$\\operatorname{IsInducing}\\bigl(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\circ F\\bigr) \\iff \\operatorname{IsInducing}\\bigl(((\\bigcup_0 \\mathcal{S}).\\mathrm{restrict}) \\circ F\\bigr)$$$
Lean4
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the topologies
of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same topology on `ι`.
In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.
This is a consequence of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsInducing`
for convenience. -/
theorem inducing_uniformOnFun_iff_pi' [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
IsInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔ IsInducing ((⋃₀ 𝔖).restrict ∘ F) :=
by
rw [isInducing_iff, isInducing_iff]
change
(_ = ((UniformOnFun.uniformSpace X α 𝔖).comap F).toTopologicalSpace) ↔
(_ = ((Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F)).toTopologicalSpace)
rw [← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]
