English
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 every K ∈ 𝔖. Then the uniform structure induced by convergence uniformly on 𝔖 coincides with the uniform structure induced by pointwise convergence on ⋃₀𝔖, i.e., the two notions give the same uniform topology on ι. In particular, pointwise convergence and compact convergence agree on equicontinuous families.
Русский
Пусть X — топологическое пространство, 𝔖 — множество компактов в X, α — равномерное пространство, и F: ι → X → α — семейство, равномерно непрерывное на каждом K ∈ 𝔖. Тогда структуры униформной сходимости по K и по точечной сходимости на ⋃₀𝔖 совпадают, т.е. одна и та же униформная структура действует на ι. В частности, для равномерно непрерывных семейств точечная и компакт-конвергенция совпадают.
LaTeX
$$$\\operatorname{IsUniformInducing}\\bigl(\\mathrm{UniformOnFun.ofFun}\\,\\mathcal{S} \\circ F\\bigr) \\;\\Longleftrightarrow\\; \\operatorname{IsUniformInducing}\\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 uniform
structures of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same
uniform structure on `ι`.
In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.
This is a version of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsUniformInducing`
for convenience. -/
theorem isUniformInducing_uniformOnFun_iff_pi' [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
IsUniformInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).restrict ∘ F) :=
by
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace, ←
EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]
rfl
