mathlib

36a20152 - feat(topology/[separation, dense_embedding]): a function to a T1 space which has a limit at x is continuous at x (#9934)

feat(topology/[separation, dense_embedding]): a function to a T1 space which has a limit at x is continuous at x (#9934) We prove that, for a function `f` with values in a T1 space, knowing that `f` admits *any* limit at `x` suffices to prove that `f` is continuous at `x`. We then use it to give a variant of `dense_inducing.extend_eq` with the same assumption required for continuity of the extension, which makes using both `extend_eq` and `continuous_extend` easier, and also brings us closer to Bourbaki who makes no explicit continuity assumption on the function to extend.