∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (x : X), Set.range f ∈ nhds (f x) → Filter.map f (nhds x) = nhds (f x)