# Zulip Chat Archive

## Stream: maths

### Topic: homeos

#### Patrick Massot (Sep 20 2018 at 20:01):

@Scott Morrison For the perfectoid project I had to get back to my old https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/homeos.lean defining homeomorphisms. But now we have the category Top in mathlib, and isomorphisms. Can I throw away my file and use the category theory stuff? How would that work?

#### Reid Barton (Sep 20 2018 at 20:06):

That's what I did in lean-homotopy-theory. My internet is acting up and I can't provide a direct link, but the filename is `src/homotopy_theory/topological_spaces/homeomorphism.lean`

#### Patrick Massot (Sep 20 2018 at 20:11):

great

#### Patrick Massot (Sep 20 2018 at 20:12):

It looks nice, but I'd like to be able to plug this into the story we have in the separation thread

#### Patrick Massot (Sep 20 2018 at 20:12):

Do you think it's possible, or does it mean everything must be rewritten in terms of Top instead of topological_space?

Last updated: May 14 2021 at 19:21 UTC