Theorem CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal

Modification history

2025-12-01 18:53
Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
feat(CategoryTheory): localization of locally presentable categories (#30554) …
Added CategoryTheory.MorphismProperty.isLocallyPresentable_isLocalView on Github →