Theorem UniformSpaceCat.extension_comp_coe

Modification history

2025-12-18 13:14
Mathlib/Topology/Category/UniformSpace.lean
refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …
Deleted UniformSpaceCat.extension_comp_coeView on Github →
2023-06-16 02:09
Mathlib/Topology/Category/UniformSpace.lean
feat: port Topology.Category.UniformSpace (#4531)
Added UniformSpaceCat.extension_comp_coeView on Github →