Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 06:05 3c2ed2ae

View on Github →

feat(topology/sheaves): construct sheaves of functions (#3608)

Sheaf conditions for presheaves of (continuous) functions.

We show that

  • Top.sheaf_condition.to_Type: not-necessarily-continuous functions into a type form a sheaf
  • Top.sheaf_condition.to_Types: in fact, these may be dependent functions into a type family
  • Top.sheaf_condition.to_Top: continuous functions into a topological space form a sheaf

Estimated changes