Theorem Topology.IsInducing.sumElim_of_separatedNhds

Modification history

2025-08-04 20:55
Mathlib/Topology/Constructions/SumProd.lean
feat: add IsEmbedding.sumElim_of_separatingNhds (#26099) …
Added Topology.IsInducing.sumElim_of_separatedNhdsView on Github →