Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-12 16:37 43bd924d

View on Github →

feat(topology/category/Profinite): iso_equiv_homeo (#7529) From LTE

Estimated changes

Modified src/topology/category/Profinite/default.lean

modified def Fintype.to_Profinite

added def Profinite.homeo_of_iso

modified theorem Profinite.is_closed_map

modified theorem Profinite.is_iso_of_bijective

added def Profinite.iso_equiv_homeo

added def Profinite.iso_of_homeo