Theorem Topology.isEmbedding_iff_isStrictMap_injective

Modification history

2026-05-12 21:04
Mathlib/Topology/Maps/Strict/Basic.lean
feat(Topology): test strictness on quotient and subspaces (#39210)
Added Topology.isEmbedding_iff_isStrictMap_injectiveView on Github →