Theorem CategoryTheory.Subobject.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀

Modification history

2026-03-31 18:15

Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean

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

Added CategoryTheory.Subobject.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀ View on Github →