Theorem TopCat.Presheaf.germ_exist_of_isBasis

Modification history

2026-05-18 11:50
Mathlib/Topology/Sheaves/Stalks.lean
feat(Stalks): add `exists_le_germ_eq` (#39490) …
Deleted TopCat.Presheaf.germ_exist_of_isBasisView on Github →
2025-05-10 07:53
Mathlib/Topology/Sheaves/Stalks.lean
feat(AlgebraicGeometry): equivalence between ideal sheaves and closed subschemes (#24615)
Added TopCat.Presheaf.germ_exist_of_isBasisView on Github →