Theorem CompHaus.Sigma.ι_comp_toFiniteCoproduct

Modification history

2024-08-01 08:35
Mathlib/Topology/Category/CompHaus/Limits.lean
refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces (#12930) …
Deleted CompHaus.Sigma.ι_comp_toFiniteCoproductView on Github →
2023-07-29 10:38
Mathlib/Topology/Category/CompHaus/Limits.lean
feat: some API for explicit limits in CompHaus (#5762) …
Added CompHaus.Sigma.ι_comp_toFiniteCoproductView on Github →