# 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.

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

- extendFrom A f x = limUnder (nhdsWithin x A) f

## Instances For

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₀`

.

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`

.

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.