Commit 2026-04-15 18:36 dc24f227

View on Github →

feat(Topology/Maps): add Bourbaki strict maps (#36660) Implements #36269.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

added theorem isHomeomorph_iff_isQuotientMap_injective

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

added theorem Topology.IsClosedMap.isStrictMap

added theorem Topology.IsOpenMap.isStrictMap

added theorem Topology.IsStrictMap.continuous

added def Topology.IsStrictMap

added theorem Topology.isStrictMap_iff_isEmbedding_kerLift

added theorem Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange

added theorem Topology.isStrictMap_iff_isQuotientMap_rangeFactorization