mathlib3

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