Theorem CategoryTheory.isLocallySurjective_iff_whisker_forget

Modification history

2024-05-30 06:23

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

feat(CategoryTheory/Sites): more properties of locally surjective morphisms of presheaves (#13318) …

Deleted CategoryTheory.isLocallySurjective_iff_whisker_forget View on Github →

2023-06-11 13:19

Mathlib/CategoryTheory/Sites/Surjective.lean

feat: port CategoryTheory.Sites.Surjective (#4969)

Added CategoryTheory.isLocallySurjective_iff_whisker_forget View on Github →