Theorem CategoryTheory.Ind.exists_nonempty_arrow_mk_iso_ind_lim

Modification history

2025-01-28 09:37
Mathlib/CategoryTheory/Limits/Indization/Category.lean
feat: equalizers and coequalizers in the category of ind-objects (#21139) …
Added CategoryTheory.Ind.exists_nonempty_arrow_mk_iso_ind_limView on Github →