mathlib documentation

topology.extend_from_subset

Extending a function from a subset

The main definition of this file is extend_from 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 analoguous to the way dense_inducing.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 continuous_on_extend_from which states that, for extend_from 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 regular space.

def extend_from {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] :
set X(X → Y)X → Y

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
theorem tendsto_extend_from {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {A : set X} {f : X → Y} {x : X} :
(∃ (y : Y), filter.tendsto f (𝓝[A] x) (𝓝 y))filter.tendsto f (𝓝[A] x) (𝓝 (extend_from A f x))

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

theorem extend_from_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [t2_space Y] {A : set X} {f : X → Y} {x : X} {y : Y} :
x closure Afilter.tendsto f (𝓝[A] x) (𝓝 y)extend_from A f x = y

theorem extend_from_extends {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [t2_space Y] {f : X → Y} {A : set X} (hf : continuous_on f A) (x : X) :
x Aextend_from A f x = f x

theorem continuous_on_extend_from {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [regular_space Y] {f : X → Y} {A B : set X} :
B closure A(∀ (x : X), x B(∃ (y : Y), filter.tendsto f (𝓝[A] x) (𝓝 y)))continuous_on (extend_from A f) B

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

theorem continuous_extend_from {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [regular_space Y] {f : X → Y} {A : set X} :
dense A(∀ (x : X), ∃ (y : Y), filter.tendsto f (𝓝[A] x) (𝓝 y))continuous (extend_from A f)

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