Def CategoryTheory.Limits.IsTerminal.isTerminalIffObj

Modification history

2024-02-01 20:02

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

feat(CategoryTheory/Galois): evaluation is injective and more basic properties (#9841) …

Added CategoryTheory.Limits.IsTerminal.isTerminalIffObj View on Github →