∀ {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_2} {M₂ : Type u_1} [inst_2 : AddCommMonoid M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} {S : Set M₁}
  (motive : (∃ K, IsCompact K ∧ ⇑f '' S ⊆ K) → Prop) (x : ∃ K, IsCompact K ∧ ⇑f '' S ⊆ K),
  (∀ (w : Set M₂) (hK : IsCompact w) (hKf : ⇑f '' S ⊆ w), motive ⋯) → motive x