Theorem CategoryTheory.GrothendieckTopology.arrows_mem_toPrecoverage_iff

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.arrows_mem_toPrecoverage_iffView on Github →