Theorem CategoryTheory.GrothendieckTopology.toPrecoverage_monotone

Modification history

2026-03-03 16:04
Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean
chore(CategoryTheory/Sites): generalize `Precoverage.toGrothendieck_le_iff_le_toPrecoverage` (#35920)
Added CategoryTheory.GrothendieckTopology.toPrecoverage_monotoneView on Github →