Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Profinite.is_iso_of_bijective

Modification history

2021-05-12 16:37
src/topology/category/Profinite/default.lean
feat(topology/category/Profinite): iso_equiv_homeo (#7529) …
Modified Profinite.is_iso_of_bijectiveView on Github →
2021-05-02 09:28
src/topology/category/Profinite.lean
feat(topology/category/Profinite): Any continuous bijection of profinite spaces is an isomorphism. (#7430)
Added Profinite.is_iso_of_bijectiveView on Github →