Def TopCat.GlueData.fromOpenSubsetsGlue

Modification history

2026-09-04 11:59

Mathlib/Topology/Gluing.lean

chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …

Modified TopCat.GlueData.fromOpenSubsetsGlue View on Github →

2023-06-14 11:40

Mathlib/Topology/Gluing.lean

feat: port Topology.Gluing (#3987)

Added TopCat.GlueData.fromOpenSubsetsGlue View on Github →