Commit 2025-02-19 16:57 757861f8
View on Github →feat: PartialHomeomorph.const (#22083) which is the constant partial homeomorphism between two open singleton sets. Step 2 of #5462, proving that discrete spaces are 0-dimensional manifolds. I'm needing this for my bordism theory project.