Commit 2025-02-24 09:31 d210fa1b

feat: discrete topological spaces are 0-manifolds (#22105) If M has the discrete topology:

• if Unique H, we provide a charted space instance ChartedSpace H M,
• if Unique E, we prove that M is a manifold w.r.t. modelWithCornersSelf 𝕜 E #5462 claimed the same for Subsingleton H (and E): this is not quite correct, as a non-empty space M is not a manifold over an empty type H. Using Unique works, however (and is equally good in practice). Fixes #5462. Part of my bordism theory project.