Theorem CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀

Modification history

2025-05-20 10:01
Mathlib/CategoryTheory/Topos/Classifier.lean
feat(CategoryTheory/Topos): add representability results for subobject classifier (#22881) …
Added CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀View on Github →