Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 14:53 480c757a

View on Github →

feat(src/topology/category/Top/limits): Coproducts in Top. (#17282)

Estimated changes

Modified src/topology/category/Top/limits.lean

added def Top.binary_cofan

added def Top.binary_cofan_is_colimit

added theorem Top.binary_cofan_is_colimit_iff

added def Top.initial_iso_pempty

added def Top.is_initial_pempty

added def Top.is_terminal_punit

added def Top.terminal_iso_punit