Zulip Chat Archive
Stream: Is there code for X?
Topic: CW Complex
Adam Dionne (Jan 21 2021 at 19:11):
Has n-dimensional CW complex (https://en.wikipedia.org/wiki/CW_complex) been formalized in Lean? What about an infinite dimensional CW complex?
Johan Commelin (Jan 21 2021 at 19:25):
@Adam Dionne Nope, we don't have CW complexes yet.
Johan Commelin (Jan 21 2021 at 19:25):
I've done simplicial sets in branch#sset and I hope to add them to mathlib at some point in the future.
Johan Commelin (Jan 21 2021 at 19:26):
@Reid Barton Or maybe you did CW in your repo? I actually don't know.
Kevin Buzzard (Jan 22 2021 at 08:18):
It's time we had these things, and also simplicial homology
Reid Barton (Jan 22 2021 at 11:43):
No, I didn't define CW complexes.
Last updated: Dec 20 2023 at 11:08 UTC