Uniform approximation by products

We show that if X, Y are compact Hausdorff spaces with X profinite, then any continuous function on X × Y valued in a ring (with a uniform structure) can be uniformly approximated by finite sums of functions of the form f x * g y.

theorem ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity {X : Type u_1} {Y : Type u_2} {R : Type u_3} {V : Type u_4} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] {S : Set (V × V)} [TopologicalSpace R] [MonoidWithZero R] [MulActionWithZero R V] (f : C(X × Y, V)) (hS : S ∈ uniformity V) : ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)), ∀ (x : X) (y : Y), (f (x, y), ∑ i : Fin n, (g i) x • (h i) y) ∈ S

A continuous function on X × Y, taking values in an R-module with a uniform structure, can be uniformly approximated by sums of functions of the form (x, y) ↦ f x • g y.

Note that no continuity properties are assumed either for multiplication on R, or for the scalar multiplication of R on V.

theorem ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [Ring R] [UniformSpace R] [IsUniformAddGroup R] (f : C(X × Y, R)) {S : Set (R × R)} (hS : S ∈ uniformity R) : ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R)), ∀ (x : X) (y : Y), (f (x, y), ∑ i : Fin n, (g i) x * (h i) y) ∈ S

A continuous function on X × Y, taking values in a ring R equipped with a uniformity compatible with addition, can be uniformly approximated by sums of functions of the form (x, y) ↦ f x * g y.

Note that no assumption is needed relating the multiplication on R to the uniformity.