Commit 2026-05-05 12:38 8e500529

View on Github →

chore(CategoryTheory/Sites/Canonical): fix universe generality (#38955) We also add one lemma about Sheaf.finestTopology. From Proetale.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

modified def CategoryTheory.Sheaf.finestTopology

modified def CategoryTheory.Sheaf.finestTopologySingle

modified theorem CategoryTheory.Sheaf.le_finestTopology

added theorem CategoryTheory.Sheaf.mem_finestTopology_of_forall_isSheafFor

modified theorem CategoryTheory.Sheaf.sheaf_for_finestTopology