∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [RegularSpace Y] {f : X → Y}
  {A : Set X}, Dense A → (∀ (x : X), ∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → Continuous (extendFrom A f)