English
Let 𝔖 be a family of compact subsets of X, F: ι → X → α equicontinuous on each K ∈ 𝔖, and a filter ℱ on ι with f : X → α. Then the following two notions of convergence are equivalent: convergence of F through UniformOnFun on 𝔖 to f via UniformOnFun, and convergence of F through restriction to ⋃₀𝔖 to f via pointwise restriction.
Русский
Пусть 𝔖 — семейство компактов X, F: ι → X → α равномерно по каждому K ∈ 𝔖, а также фильтр ℱ на ι и функция f. Тогда эквивалентны две формы сходимости: через UniformOnFun и через ограничение на ⋃₀𝔖.
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 \n\\operatorname{Tendsto}\\bigl(((\\bigcup_0 \\mathcal{S}).\\restrict) \\circ F\\bigr)\\;\\mathcal{F}\\; (\\mathcal{N}\\bigl(((\\bigcup_0 \\mathcal{S}).\\restrict)\\; f \\bigr))$$
Lean4
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`,
`α` 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 on `⋃₀ 𝔖`* along `ℱ`. -/
theorem tendsto_uniformOnFun_iff_pi' {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α) :
Tendsto (UniformOnFun.ofFun 𝔖 ∘ F) ℱ (𝓝 <| UniformOnFun.ofFun 𝔖 f) ↔
Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (𝓝 <| (⋃₀ 𝔖).restrict f) :=
by
-- Recall that the uniform structure on `X →ᵤ[𝔖] α` is the one induced by all the maps
-- `K.restrict : (X →ᵤ[𝔖] α) → (K →ᵤ α)` for `K ∈ 𝔖`.
-- Similarly, the uniform structure on `X → α` induced by the map
-- `(⋃₀ 𝔖).restrict : (X → α) → ((⋃₀ 𝔖) → α)` is equal to the one induced by
-- all maps `K.restrict : (X → α) → (K → α)` for `K ∈ 𝔖`
-- Thus, we just have to compare the two sides of our goal when restricted to some
-- `K ∈ 𝔖`, where we can apply `Equicontinuous.tendsto_uniformFun_iff_pi`.
rw [← Filter.tendsto_comap_iff (g := (⋃₀ 𝔖).restrict), ← nhds_induced]
simp_rw [UniformOnFun.topologicalSpace_eq, Pi.induced_restrict_sUnion 𝔖 (A := fun _ ↦ α), _root_.nhds_iInf,
nhds_induced, tendsto_iInf, tendsto_comap_iff]
congrm ∀ K (hK : K ∈ 𝔖), ?_
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
rw [← (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).tendsto_uniformFun_iff_pi]
rfl
