Commit 2025-03-17 06:31 be97c7f8

feat: Fin.init and Fin.tail are continuous (#22550) I needed the continuity of Fin.init for the inductive CW structure on the sphere. There the inverses of the characteristic maps are just the projections of the upper and lower hemisphere onto the obvious hyperplane. It was easiest to use Fin.init for this.