# Commit 2020-08-05 22:44 2918b00b

View on Github →feat(topology): define `extend_from`

, add lemmas about extension by continuity on sets and intervals and continuity gluing (#3590)

#### Add a new file `topology/extend_from_subset`

(mostly by @PatrickMassot )

Define `extend_from A f`

(where `f : X → Y`

and `A : set X`

) to be a function `g : X → Y`

which maps any
`x₀ : X`

to the limit of `f`

as `x`

tends to `x₀`

, if such a limit exists. Although this is not really an extension, it maps with the classical meaning of extending a function *defined on a set*, hence the name. In some way it is analogous to `dense_inducing.extend`

, but in `set`

world.
The main theorem about this is `continuous_on_extend_from`

about extension by continuity

#### Corollaries for extending functions defined on intervals

A few lemmas of the form : if `f`

is continuous on `Ioo a b`

, then `extend_from (Ioo a b) f`

is continuous on `I[cc/co/oc] a b`

, provided some assumptions about limits on the boundary (and has some other properties, e.g it is equal to `f`

on `Ioo a b`

)

#### More general continuity gluing

Lemmas `continuous_on_if'`

and its corollaries `continuous_on_if`

and `continuous_if'`

, and a few other continuity lemmas