Theorem TopCat.GlueData.open_image_open

Modification history

2024-12-10 02:59

Mathlib/Topology/Gluing.lean

chore: address and delete many porting notes across the library (#19685)

Modified TopCat.GlueData.open_image_open View on Github →

2023-06-14 11:40

Mathlib/Topology/Gluing.lean

feat: port Topology.Gluing (#3987)

Added TopCat.GlueData.open_image_open View on Github →