Theorem dense_inducing.extend_eq_at'

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