Theorem CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_mono_not_isIso

Modification history

2025-10-29 00:03
Mathlib/CategoryTheory/Generator/StrongGenerator.lean
feat(CategoryTheory): strong generators (#29519) …
Added CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_mono_not_isIsoView on Github →