Theorem CategoryTheory.Functor.initial_fromPUnit_of_isInitial

Modification history

2025-05-13 20:30

Mathlib/CategoryTheory/Limits/Final.lean

feat(CategoryTheory/Limits/Final): `fromPUnit c` is final if `c` is terminal (#24847) …

Added CategoryTheory.Functor.initial_fromPUnit_of_isInitial View on Github →