Theorem TopCat.Presheaf.exists_mem_germ_eq_of_isBasis

Modification history

2026-05-18 11:50
Mathlib/Topology/Sheaves/Stalks.lean
feat(Stalks): add `exists_le_germ_eq` (#39490) …
Added TopCat.Presheaf.exists_mem_germ_eq_of_isBasisView on Github →