∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyCoherentSpace X] (s : Set X),
  IsOpen s ↔ ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)