mathlib

49e0bcfe - feat(topology/bases): continuous_of_basis_is_open_preimage (#9281)

feat(topology/bases): continuous_of_basis_is_open_preimage (#9281) Check continuity on a basis. Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>