mathlib3

2918b00b - feat(topology): define `extend_from`, add lemmas about extension by continuity on sets and intervals and continuity gluing (#3590)

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 Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>