Theorem isEmbedding_sumElim

Modification history

2025-08-04 20:55

Mathlib/Topology/Constructions/SumProd.lean

feat: add IsEmbedding.sumElim_of_separatingNhds (#26099) …

Added isEmbedding_sumElim View on Github →