mathlib

1539ee18 - refactor(topology/sheaves/*): Make sheaf condition a Prop (#9607)

refactor(topology/sheaves/*): Make sheaf condition a Prop (#9607) Make `sheaf_condition` into a `Prop` and redefine the type of sheaves on a topological space `X` as a subtype of `(opens X)ᵒᵖ ⥤ C`.