Theorem CategoryTheory.MorphismProperty.exists_map_eq_of_presieve

Modification history

2026-03-04 16:50
Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean
feat(CategoryTheory/MorphismProperty): API for sites on `P.Over ⊤ X` (#36126) …
Added CategoryTheory.MorphismProperty.exists_map_eq_of_presieveView on Github →