Def CompHausLike.productIsLimit

Modification history

2025-12-19 10:23

Mathlib/Topology/Category/CompHausLike/Cartesian.lean

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

Modified CompHausLike.productIsLimit View on Github →

2025-11-24 05:14

Mathlib/Topology/Category/CompHausLike/Cartesian.lean

feat(Condensed): cartesian monoidal functor LightProfinite -> LightCondSet (#30800)

Added CompHausLike.productIsLimit View on Github →