English
Let X be a space, 𝔖 a covering of X by compact subsets, α a uniform space, and F: ι → X → α equicontinuous on each K ∈ 𝔖. Then the uniform structure induced by uniform convergence on 𝔖 is uniformly inducible to ι if and only if the uniform structure induced by pointwise convergence on the same data is. In particular, the two notions agree under a covering assumption.
Русский
Пусть X — пространство, 𝔖 — покрытие X компактными подмножествами, α — униформное пространство, и F: ι → X → α равномерно непрерывно по каждому K ∈ 𝔖. Тогда структуры униформной сходимости по 𝔖 и точечной по тем же данным согласованы по умолчанию: две эти структуры порождают одну и ту же униформную структуру на ι, когда 𝔖 образует покрытие.
LaTeX
$$$\\operatorname{IsUniformInducing}\\bigl(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\circ F\\bigr) \\iff \\operatorname{IsUniformInducing}(F)$$$
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 uniform
structures of uniform convergence on `𝔖` and pointwise convergence induce the same
uniform structure on `ι`.
This is a specialization of `EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'` to
the case where `𝔖` covers `X`. -/
theorem isUniformInducing_uniformOnFun_iff_pi [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = univ)
(𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
IsUniformInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔ IsUniformInducing F :=
by
rw [eq_univ_iff_forall] at 𝔖_covers
let φ : ((⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (β := fun _ ↦ α) (Equiv.subtypeUnivEquiv 𝔖_covers)
rw [EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]
exact ⟨fun H ↦ φ.isUniformInducing.comp H, fun H ↦ φ.symm.isUniformInducing.comp H⟩
