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