Commit 2025-08-04 20:55 2c4e63c0
View on Github →feat: add IsEmbedding.sumElim_of_separatingNhds (#26099) Characterise when the Sum.elim of two inducing maps resp. embeddings is an embedding, and deduce that the ranges of the two maps lying in separated neighbourhoods suffices. This is used in my bordism theory project. Co-authored by: @plp127