Def CompHausLike.coproductCocone

Modification history

2026-09-04 11:59

Mathlib/Topology/Category/CompHausLike/Cartesian.lean

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

Modified CompHausLike.coproductCocone View on Github →

2025-12-19 10:23

Mathlib/Topology/Category/CompHausLike/Cartesian.lean

feat(Topology/Category): explicit binary coproducts in `CompHausLike` (#32914) …

Added CompHausLike.coproductCocone View on Github →