CW Complexes

Stream: Is there code for X?

[Archie Browne]

Hi all, I was wondering about CW complexes in Lean. I understand there has been attempts to formalise the before but they were difficult for various reasons. What has been tried and what were the tricky parts in these cases. Thanks.

[Junyan Xu]

This thread contains some early attempts, and this post says a definition will be submitted as a pull request soon.

[Archie Browne]

@Junyan Xu Okay Thanks!

[Dean Young]

@Archie Browne thanks for your interest Archie. Jiazhen and I are going a bit slowly but we can go ahead and add in the definitions now I think :-)