∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (y : Y),
  Filter.Tendsto (⇑f) (Filter.coclosedCompact X) (nhds y) → Continuous fun x => x.elim y ⇑f