Commit 2026-05-18 11:50 0549d809

View on Github →

feat(Stalks): add exists_le_germ_eq (#39490) Also rename germ_exist to exists_germ_eq to follow the naming convention. Motivated by the Cauchy theorem project at ICERM workshop "Techniques and Tools for the Formalization of Analysis".

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/Basic.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Topology/Sheaves/LocallySurjective.lean

Modified Mathlib/Topology/Sheaves/Sheafify.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.exists_germ_eq

added theorem TopCat.Presheaf.exists_le_germ_eq

added theorem TopCat.Presheaf.exists_mem_germ_eq_of_isBasis

deleted theorem TopCat.Presheaf.germ_exist

deleted theorem TopCat.Presheaf.germ_exist_of_isBasis