Theorem CategoryTheory.Precoverage.toGrothendieck_mono

Modification history

2026-03-03 16:04

Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

chore(CategoryTheory/Sites): generalize `Precoverage.toGrothendieck_le_iff_le_toPrecoverage` (#35920)

Modified CategoryTheory.Precoverage.toGrothendieck_mono View on Github →

2026-02-07 07:45

Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

feat(CategoryTheory/Sites): various API additions for #34917 (#34921)

Added CategoryTheory.Precoverage.toGrothendieck_mono View on Github →