Commit 2026-05-12 21:04 e3960f5c

View on Github →

feat(Topology): test strictness on quotient and subspaces (#39210)

Estimated changes

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/Maps/Basic.lean

Modified Mathlib/Topology/Maps/Strict/Basic.lean

added theorem Topology.IsEmbedding.isStrictMap

added theorem Topology.IsEmbedding.isStrictMap_iff

added theorem Topology.IsHomeomorph.isStrictMap

added theorem Topology.IsQuotientMap.isStrictMap

added theorem Topology.IsQuotientMap.isStrictMap_iff

added theorem Topology.IsStrictMap.id

added theorem Topology.isEmbedding_iff_isStrictMap_injective

added theorem Topology.isQuotientMap_iff_isStrictMap_surjective