Commit 2025-08-31 09:05 21a397a9

View on Github →

chore(CategoryTheory/Sites): rename Presieve.isSeparated_of_isSheaf -> Presieve.IsSheaf.isSeparated (#29088) Rename Presieve.isSeparated_of_isSheaf to Presieve.IsSheaf.isSeparated to enable dot notation. I've also made the arguments J and P implicit, since they can be inferred from h : IsSheaf J P.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

Modified Mathlib/CategoryTheory/Sites/CoversTop.lean

Modified Mathlib/CategoryTheory/Sites/LocallyBijective.lean

Modified Mathlib/CategoryTheory/Sites/LocallyInjective.lean

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

added theorem CategoryTheory.Presieve.IsSheaf.isSeparated

deleted theorem CategoryTheory.Presieve.isSeparated_of_isSheaf

Modified Mathlib/CategoryTheory/Sites/Whiskering.lean