Def CategoryTheory.Classifier.mkOfTerminalΩ₀

Modification history

2025-07-15 08:52

Mathlib/CategoryTheory/Topos/Classifier.lean

feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …

Added CategoryTheory.Classifier.mkOfTerminalΩ₀ View on Github →