∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] (f : M₁ → M₂) (motive : IsCompactOperator f → Prop) (x : IsCompactOperator f),
  (∀ (K : Set M₂) (hK : IsCompact K) (hKf : f ⁻¹' K ∈ nhds 0), motive ⋯) → motive x