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 (𝓝[A] x) 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.