Commit 2026-03-03 16:04 6d653853

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

deleted theorem CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff

deleted def CategoryTheory.GrothendieckTopology.toPrecoverage

deleted theorem CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

added theorem CategoryTheory.GrothendieckTopology.arrows_mem_toPrecoverage_iff

added theorem CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff

added theorem CategoryTheory.GrothendieckTopology.toGrothendieck_toPrecoverage_le

added def CategoryTheory.GrothendieckTopology.toPrecoverage

added theorem CategoryTheory.GrothendieckTopology.toPrecoverage_monotone

added theorem CategoryTheory.GrothendieckTopology.toPrecoverage_top

added theorem CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage

added theorem CategoryTheory.Precoverage.le_toPrecoverage_toGrothendieck

added theorem CategoryTheory.Precoverage.toGrothendieck_bot

added theorem CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage

modified theorem CategoryTheory.Precoverage.toGrothendieck_mono

added theorem CategoryTheory.Precoverage.toGrothendieck_monotone