mathlib
a1b73125 - feat(topology/maps): a few lemmas about `is_open_map` (#1855)

Commit
6 years ago
feat(topology/maps): a few lemmas about `is_open_map` (#1855) * feat(topology/maps): a few lemmas about `is_open_map` Also fix arguments order in all `*.comp` in this file. * Use restricted version of `continuous_of_left_inverse` to prove non-restricted * Fix compile by reverting a name change
Author
Committer
Parents
Loading