Commit 2025-06-12 17:36 079d9079

View on Github →

chore(CategoryTheory/Sites/Preserves): generalize universes (#25764) ... and remove two erws on the way.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

modified theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff

added theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small

Modified Mathlib/CategoryTheory/Sites/Preserves.lean