Products of von Neumann bounded sets #
A product s ×ˢ t of von Neumann bounded subsets of two topological spaces with a 𝕜-action is
von Neumann bounded in the product space. This is used to check the boundedness condition in
Mathlib's Bundle.RiemannianMetric for the product of two Riemannian metrics.
theorem
Bornology.IsVonNBounded.prod
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[SeminormedRing 𝕜]
[Zero E]
[SMul 𝕜 E]
[TopologicalSpace E]
[Zero F]
[SMul 𝕜 F]
[TopologicalSpace F]
{s : Set E}
{t : Set F}
(hs : IsVonNBounded 𝕜 s)
(ht : IsVonNBounded 𝕜 t)
:
IsVonNBounded 𝕜 (s ×ˢ t)
A product of von Neumann bounded sets is von Neumann bounded.