Theorem filter.map_id'

feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753) …