ι : Type ?u.168240
α : Type ?u.168243
X : Type ?u.168246
M : Type u_1
N : Type ?u.168252
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.fst * x.snd) '' s ×ˢ t)
ι : Type ?u.168240
α : Type ?u.168243
X : Type ?u.168246
M : Type u_1
N : Type ?u.168252
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)
rw [← image_mul_prod]
no goals
ι : Type ?u.168240
α : Type ?u.168243
X : Type ?u.168246
M : Type u_1
N : Type ?u.168252
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.fst * x.snd) '' s ×ˢ t)
exact (hs.prod ht).image continuous_mul