Diagonal extraction for uniform convergence with values in a uniform space

A countable family of sets S j and a sequence f : ℕ → X → α are given, together with the ability to refine any subsequence into a further subsequence that converges uniformly on a prescribed S j. A single subsequence then converges uniformly on every S j, with one limit function shared by all of them.

The limit is recovered as the pointwise limit of the diagonal subsequence, which is where the Hausdorff hypothesis on the target enters: the uniform limits produced on the separate sets S j agree wherever they overlap because each of them is the pointwise limit of the same sequence.

The target is any Hausdorff uniform space, so the statement applies to real-valued families, to families of continuous linear maps, and to tuples of both — the combination needed to extract a C¹ limit of a sequence of functions together with its derivative along one subsequence.

theorem CIV.exists_subseq_tendstoUniformlyOn_forall_of_subseq {X : Type u_1} {α : Type u_2} [UniformSpace α] [T2Space α] [Nonempty α] (S : ℕ → Set X) (f : ℕ → X → α) (hstep : ∀ (j : ℕ) (g : ℕ → ℕ), StrictMono g → ∃ (g' : ℕ → ℕ), StrictMono g' ∧ ∃ (w : X → α), TendstoUniformlyOn (fun (n : ℕ) => f (g (g' n))) w Filter.atTop (S j)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (w : X → α), ∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => f (φ n)) w Filter.atTop (S j)

Diagonal extraction over a countable family of sets, for values in a Hausdorff uniform space: if from every subsequence one can extract a further subsequence converging uniformly on S j, then a single subsequence converges uniformly on every S j, with one limit function.