Commit 2021-10-26 21:02 36a20152

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.