Mathlib Changelog
Changelog
About
Github
Commit
2022-01-28 03:07
f5d63f9f
View on Github →
feat(topology/category/Compactum): forget creates limits (
#11690
) Will likely be used in LTE.
Estimated changes
Modified
src/topology/category/Compactum.lean
added
def
Compactum_to_CompHaus_comp_forget