English
Let 𝔖 be a covering of X by compact subsets, α a uniform space, and F: ι → X → α equicontinuous on each K ∈ 𝔖. Then Tendsto(UniformOnFun.ofFun 𝔖 ∘ F) ℱ (𝓝 (UniformOnFun.ofFun 𝔖 f)) is equivalent to Tendsto F ℱ (𝓝 f).
Русский
Пусть 𝔖 — покрытие X компактными подмножествами, α — униформное пространство, F: ι → X → α равномерно по каждому K ∈ 𝔖. Тогда сходимость через UniformOnFun эквивалентна по точечной схеме обычной сходимости для F.
LaTeX
$$$\\operatorname{Tendsto}\\bigl(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\circ F\\bigr)\\;\\mathcal{F}\\; (\\mathcal{N}\\bigl(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\; f\\bigr)) \\iff \\operatorname{Tendsto} F\\;\\mathcal{F}\\; (\\mathcal{N} f)$$$
Lean4
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets,
`α` a uniform space, `F : ι → (X → α)` a family equicontinuous on each `K ∈ 𝔖`, and `ℱ` a filter
on `ι`. Then, `F` tends to `f : X → α` along `ℱ` *uniformly on each `K ∈ 𝔖`* iff it tends to `f`
*pointwise* along `ℱ`.
This is a specialization of `EquicontinuousOn.tendsto_uniformOnFun_iff_pi'` to the case
where `𝔖` covers `X`. -/
theorem tendsto_uniformOnFun_iff_pi {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = univ)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α) :
Tendsto (UniformOnFun.ofFun 𝔖 ∘ F) ℱ (𝓝 <| UniformOnFun.ofFun 𝔖 f) ↔ Tendsto F ℱ (𝓝 f) :=
by
rw [eq_univ_iff_forall] at 𝔖_covers
let φ : ((⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Y := fun _ ↦ α) (Equiv.subtypeUnivEquiv 𝔖_covers)
rw [EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont, show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl,
show restrict (⋃₀ 𝔖) f = φ.symm f by rfl, φ.symm.isInducing.tendsto_nhds_iff]
