Commit 2024-07-05 14:52 a16b3ecd

View on Github →

chore(CategoryTheory/Sites): saturate -> Saturate (#14449) The old name didn't follow the naming convention, since it's a function taking values in Prop

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/RegularTopology.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

added inductive CategoryTheory.Coverage.Saturate

deleted inductive CategoryTheory.Coverage.saturate