Theorem CategoryTheory.Presieve.pullback_singleton

Modification history

2025-08-30 20:46

Mathlib/CategoryTheory/Sites/Sieves.lean

refactor(CategoryTheory/Sites/Sieves): avoid `HasPullbacks C` in `Presieve.pullbackArrows` (#29085) …

Modified CategoryTheory.Presieve.pullback_singleton View on Github →

2023-03-07 13:26

Mathlib/CategoryTheory/Sites/Sieves.lean

feat: port CategoryTheory.Sites.Sieves (#2691)

Added CategoryTheory.Presieve.pullback_singleton View on Github →