Documentation

Mathlib.Topology.Sheaves.Init

Rule sets related to topological (pre)sheaves #

This module defines the Restrict Aesop rule set. Aesop rule sets only become visible once the file in which they're declared is imported, so we must put this declaration into its own file.