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 uniform convergence topology on 𝔖 induces the same topology on ι as the pointwise convergence topology, since 𝔖 covers X.
Русский
Пусть 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 covering of `X` by compact subsets, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the topologies
of uniform convergence on `𝔖` and pointwise convergence induce the same topology on `ι`.
This is a specialization of `EquicontinuousOn.inducing_uniformOnFun_iff_pi'` to
the case where `𝔖` covers `X`. -/
theorem isInducing_uniformOnFun_iff_pi [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = univ)
(𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
IsInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔ IsInducing F :=
by
rw [eq_univ_iff_forall] at 𝔖_covers
let φ : ((⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Y := fun _ ↦ α) (Equiv.subtypeUnivEquiv 𝔖_covers)
rw [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont, show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]
exact
⟨fun H ↦ φ.isInducing.comp H, fun H ↦ φ.symm.isInducing.comp H⟩
-- TODO: find a way to factor common elements of this proof and the proof of
-- `EquicontinuousOn.comap_uniformOnFun_eq`
