Theorem CategoryTheory.Classifier.isTerminalFrom_eq_χ₀

Modification history

2025-07-15 08:52
Mathlib/CategoryTheory/Topos/Classifier.lean
feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …
Added CategoryTheory.Classifier.isTerminalFrom_eq_χ₀View on Github →