Zulip Chat Archive

Stream: maths

Topic: Alexandrov-discrete spaces

Yaël Dillies (Sep 05 2023 at 22:23):

I just finished proving that Alexandrov-discrete spaces are categorically equivalent to preorders:

def alexDiscEquivPreord : AlexDisc ≌ PreordCat

It's not very hard (I started this morning after all) but I was pleasantly surprised to see aesop come in handy a few times. The where syntax is nice too, although it sadly seems we can't nest it?

Yaël Dillies (Sep 05 2023 at 22:24):

Watch out for PRs in the next few days.

Jireh Loreaux (Sep 05 2023 at 22:41):

Yeah, the lack of nesting of where syntax is sad. :cry:

Yaël Dillies (Sep 06 2023 at 10:57):

#6980
#6981
#6982
#6985
#6986
#6988
#6989

EDIT: Now all merged!

Yaël Dillies (Sep 21 2023 at 10:32):

All PRs in now. Thanks Johan!

Last updated: Dec 20 2023 at 11:08 UTC