Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.left_inverse.closed_embedding

Modification history

2021-02-24 06:44
src/topology/separation.lean
feat(topology/separation): a cont. function with a cont. left inverse is a closed embedding (#6329)
Added function.left_inverse.closed_embeddingView on Github →