Theorems · Theorem · general topology

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} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] [inst_4 : TopologicalSpace Y] [CompactSpace Y] [inst_6 : AddCommGroup V]
  [inst_7 : UniformSpace V] [IsUniformAddGroup V] {S : Set (V × V)} [inst_9 : TopologicalSpace R]
  [inst_10 : MonoidWithZero R] [inst_11 : MulActionWithZero R V] (f : C(X × Y, V)),
  S ∈ uniformity V → ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (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.

Defined in

Mathlib.Topology.UniformSpace.ProdApproximation

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTotallyDisconnectedSpaceT2SpaceCompactSpaceTopologicalSpaceCompactSpaceAddCommGroupUniformSpaceIsUniformAddGroupTopologicalSpaceMonoidWithZeroMulActionWithZero