Theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc

Modification history

2025-12-11 00:39
Mathlib/CategoryTheory/Sites/Point/Basic.lean
feat(CategoryTheory/Sites): the category structure on the points of a site (#31711)
Added CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDescView on Github →