∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] {k : Set M} {u : Set X}, IsCompact k → IsCompact u → IsCompact (k • u)