Commit 2025-12-19 10:23 82fd6d36

View on Github →

feat(Topology/Category): explicit binary coproducts in CompHausLike (#32914) From LeanCondensed

Estimated changes

Modified Mathlib/Topology/Category/CompHausLike/Cartesian.lean

added def CompHausLike.coproductCocone

added def CompHausLike.coproductIsColimit

modified def CompHausLike.productIsLimit