Theorems · Theorem · general topology

continuous_extendFrom

∀ {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)

If a function f to a T₃ space Y has a limit within a dense set A for any x, then extendFrom A f is continuous.

Defined in

Mathlib.Topology.ExtendFrom

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceRegularSpace