Theorem Topology.isQuotientMap_iff_isStrictMap_surjective

Modification history

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