Theorem CategoryTheory.Functor.final_fromPUnit_of_isTerminal

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.final_fromPUnit_of_isTerminalView on Github →