α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo ((fun x => x.fst * x.snd) '' s ×ˢ t)
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo (s * t)
rw [← image_mul_prod]
no goals
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo ((fun x => x.fst * x.snd) '' s ×ˢ t)
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)