Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-07 23:41 45f95448

View on Github →

feat(topology/separation): an injective map on a compact space is an embedding (#6057)

Estimated changes