Theorems · Theorem · general topology

continuousOn_extendFrom

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

If f is a function to a T₃ space Y which has a limit within A at any point of a set B ⊆ closure A, then extendFrom A f is continuous on B.

Defined in

Mathlib.Topology.ExtendFrom

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceRegularSpace