mathlib3

95cc1b11 - refactor(topology/dense_embedding): simplify proof (#3329)

refactor(topology/dense_embedding): simplify proof (#3329) Using filter bases, we can give a cleaner proof of continuity of extension by continuity. Also switch to use the "new" `continuous_at` in the statement.