English
For a continuous map f: X×Y → R into a ring R with a uniform structure, there exists a finite sum approximation of the same form as above using multiplication instead of scalar action.
Русский
Для непрерывного отображения f: X×Y → R в кольцо R с униформной структурой существует конечная сумма аппроксимации аналогично предыдущему случаю с умножением вместо действия.
LaTeX
$$$\\exists n\\, (g: Fin n \\to C(X, R))\\, (h: Fin n \\to C(Y, R))\\; \\forall x,y, (f(x,y), \\sum_i g_i(x) \\cdot h_i(y)) \\in S$$$
Lean4
/-- 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. -/
theorem exists_finite_sum_mul_approximation_of_mem_uniformity [Ring R] [UniformSpace R] [IsUniformAddGroup R]
(f : C(X × Y, R)) {S : Set (R × R)} (hS : S ∈ 𝓤 R) :
∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R)), ∀ x y, (f (x, y), ∑ i, g i x * h i y) ∈ S :=
exists_finite_sum_smul_approximation_of_mem_uniformity f hS
