no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
h : Bounded (s ×ˢ t)
ht : Set.Nonempty t
⊢ Bounded s
simpa only [fst_image_prod s ht] using (@LipschitzWith.prod_fst α β _ _).bounded_image h