Commit 2024-04-09 23:35 09ed129d

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Final.lean

deleted theorem CategoryTheory.Functor.Final.colimit_pre_is_iso_aux

deleted theorem CategoryTheory.Functor.Initial.limit_pre_is_iso_aux

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean