{X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) →
      (x : ↑X) →
        CategoryTheory.Functor (TopologicalSpace.OpenNhds x)
          (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))