∀ {α : Type u_1} [inst : OmegaCompletePartialOrder α] [inst_1 : TopologicalSpace α]
  [Topology.IsScott α (Set.range fun c => Set.range ⇑c)] {f : α → Prop},
  OmegaCompletePartialOrder.ωScottContinuous f = Continuous f