mathlib3
6cb52e67 - feat(category_theory/limits): Results about (co)limits in Top (#9985)

Commit
4 years ago
feat(category_theory/limits): Results about (co)limits in Top (#9985) - Provided the explicit topologies for limits and colimits, and specialized this result onto some shapes. - Provided the isomorphism between the (co)limits and the constructions in `topology/constructions.lean`. - Provided conditions about whether `prod.map` and `pullback_map` are inducing, embedding, etc. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
Author
Parents
Loading