Theorem Topology.IsInducing.Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap

Modification history

2025-02-20 10:22
Mathlib/Topology/Maps/Basic.lean
feat: add Is{Open,Closed}Embedding.sum_elim (#22070) …
Added Topology.IsInducing.Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMapView on Github →