Theorem CategoryTheory.GlueData.types_ι_jointly_surjective

Modification history

2023-11-16 11:33
Mathlib/CategoryTheory/GlueData.lean
chore(CategoryTheory): universe polymorphic `CategoryTheory.Limits.Types.coproductIso` (#8421) …
Modified CategoryTheory.GlueData.types_ι_jointly_surjectiveView on Github →
2023-08-10 19:52
Mathlib/CategoryTheory/GlueData.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified CategoryTheory.GlueData.types_ι_jointly_surjectiveView on Github →
2023-03-26 21:07
Mathlib/CategoryTheory/GlueData.lean
feat: port CategoryTheory.GlueData (#3099)
Added CategoryTheory.GlueData.types_ι_jointly_surjectiveView on Github →