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.
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
- extend_from A f = λ (x : X), lim (nhds_within x A) f
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₀.
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.
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.