Theorem CategoryTheory.HasClassifier.isPullback_χ

Modification history

2025-07-15 08:52

Mathlib/CategoryTheory/Topos/Classifier.lean

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

Modified CategoryTheory.HasClassifier.isPullback_χ View on Github →

2025-02-24 22:30

Mathlib/CategoryTheory/Topos/Classifier.lean

feat(CategoryTheory): Define subobject classifier (#21281) …

Added CategoryTheory.HasClassifier.isPullback_χ View on Github →