Commit 2025-02-07 15:17 44291124

View on Github →

chore(CategoryTheory/Sites): fix names (#21540) imagePresheaf was renamed Subpresheaf.range in #21047. This PR fixes the names of the lemmas referring to the old name.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

deleted theorem CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top'

deleted theorem CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top

added theorem CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top'

added theorem CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top