Theorem CategoryTheory.isRepresentable_hasClassifier_iff

Modification history

2026-03-31 18:15

Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean

chore(CategoryTheory/Classifier): namespace Classifier, rename HasClassifier, move file (#36060) …

Deleted CategoryTheory.isRepresentable_hasClassifier_iff View on Github →

2025-05-20 10:01

Mathlib/CategoryTheory/Topos/Classifier.lean

feat(CategoryTheory/Topos): add representability results for subobject classifier (#22881) …

Added CategoryTheory.isRepresentable_hasClassifier_iff View on Github →