Theorem IsOpenQuotientMap.prodMap

Modification history

2025-03-11 15:38

Mathlib/Topology/Constructions.lean

chore(Topology/Constructions): split out results about sums, products and distributivity (#22827) …

Modified IsOpenQuotientMap.prodMap View on Github →

2024-09-28 09:50

Mathlib/Topology/Constructions.lean

feat(Topology): define `IsOpenQuotientMap` (#16549)

Added IsOpenQuotientMap.prodMap View on Github →