Theorem TopCat.colimit_isOpen_iff

Modification history

2024-05-02 22:40

Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

chore(Topology/Category): remove `ProfiniteMax` and `CompHausMax` (#12599) …

Modified TopCat.colimit_isOpen_iff View on Github →

2023-05-12 18:40

Mathlib/Topology/Category/Top/Limits/Pullbacks.lean

feat: port Topology.Category.Top.Limits.Pullbacks (#3802)

Added TopCat.colimit_isOpen_iff View on Github →