mathlib
64fdfc74 - feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413)

Commit

4 years ago

feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413) For the LTE: alternate constructors for presieves which can be more convenient.

Author

b-mehta

Parents

4722dd46

mathlib 64fdfc74 - feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413)

mathlib
64fdfc74 - feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413)