Theorem CategoryTheory.HasClassifier.unique

Modification history

2025-07-25 22:49
Mathlib/CategoryTheory/Topos/Classifier.lean
chore: fix more indentation (#27494) …
Modified CategoryTheory.HasClassifier.uniqueView on Github →
2025-07-15 08:52
Mathlib/CategoryTheory/Topos/Classifier.lean
feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …
Modified CategoryTheory.HasClassifier.uniqueView on Github →
2025-02-24 22:30
Mathlib/CategoryTheory/Topos/Classifier.lean
feat(CategoryTheory): Define subobject classifier (#21281) …
Added CategoryTheory.HasClassifier.uniqueView on Github →