Theorem CategoryTheory.Functor.Initial.limit_pre_is_iso_aux

Modification history

2024-04-09 23:35

Mathlib/CategoryTheory/Limits/Final.lean

chore(CategoryTheory): remove some unnecessary lemmas about final/initial functors (#12024)

Deleted CategoryTheory.Functor.Initial.limit_pre_is_iso_aux View on Github →

2023-03-13 13:03

Mathlib/CategoryTheory/Limits/Final.lean

feat: port CategoryTheory.Limits.Final (#2820)

Added CategoryTheory.Functor.Initial.limit_pre_is_iso_aux View on Github →