Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-02 09:28 4bd1c836

View on Github →

feat(topology/category/Profinite): Any continuous bijection of profinite spaces is an isomorphism. (#7430)

Estimated changes

Modified src/topology/category/CompHaus.lean

added theorem CompHaus.is_closed_map

added theorem CompHaus.is_iso_of_bijective

added def CompHaus.iso_of_bijective

Modified src/topology/category/Profinite.lean

added theorem Profinite.is_closed_map

added theorem Profinite.is_iso_of_bijective

modified def Profinite.to_Profinite_adj_to_CompHaus