Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
function.left_inverse.closed_range
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_range
View on Github →