Commit 2022-10-27 07:38 06c75afe

View on Github →

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

Modified src/topology/sheaves/presheaf.lean

added theorem Top.presheaf.map_restrict

added def Top.presheaf.restrict

added def Top.presheaf.restrict_open

added theorem Top.presheaf.restrict_restrict