no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
⊢ Bounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ Bounded s ∧ Bounded t
simp only [bounded_iff_isBounded, Bornology.isBounded_prod]