Documentation

Mathlib.Topology.ExtendFrom

Extending a function from a subset #

The main definition of this file is extendFrom A f where f : X → Y and A : Set X. This defines a new function g : X → Y which maps any x₀ : X to the limit of f as x tends to x₀, if such a limit exists.

This is analogous to the way DenseInducing.extend "extends" a function f : X → Z to a function g : Y → Z along a dense inducing i : X → Y.

The main theorem we prove about this definition is continuousOn_extendFrom which states that, for extendFrom A f to be continuous on a set B ⊆ closure A, it suffices that f converges within A at any point of B, provided that f is a function to a T₃ space.

def extendFrom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (A : Set X) (f : XY) :
XY

Extend a function from a set A. The resulting function g is such that at any x₀, if f converges to some y as x tends to x₀ within A, then g x₀ is defined to be one of these y. Else, g x₀ could be anything.

Equations
Instances For
    theorem tendsto_extendFrom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A : Set X} {f : XY} {x : X} (h : ∃ (y : Y), Filter.Tendsto f (nhdsWithin x A) (nhds y)) :

    If f converges to some y as x tends to x₀ within A, then f tends to extendFrom A f x as x tends to x₀.

    theorem extendFrom_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {A : Set X} {f : XY} {x : X} {y : Y} (hx : x closure A) (hf : Filter.Tendsto f (nhdsWithin x A) (nhds y)) :
    extendFrom A f x = y
    theorem extendFrom_extends {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} {A : Set X} (hf : ContinuousOn f A) (x : X) :
    x AextendFrom A f x = f x
    theorem continuousOn_extendFrom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {f : XY} {A : Set X} {B : Set X} (hB : B closure A) (hf : xB, ∃ (y : Y), Filter.Tendsto f (nhdsWithin x A) (nhds y)) :

    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.

    theorem continuous_extendFrom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {f : XY} {A : Set X} (hA : Dense A) (hf : ∀ (x : X), ∃ (y : Y), Filter.Tendsto f (nhdsWithin x A) (nhds y)) :

    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.