Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-15 10:30 9ba9a983

View on Github →

chore(category_theory/sites): improve naming (#5350)

Improve naming of some lemmas to be more descriptive
Golf some proofs
Add some convenience deconstructors which are useful in practice

Estimated changes

Modified src/category_theory/sites/canonical.lean

Modified src/category_theory/sites/sheaf.lean

added theorem category_theory.presieve.is_separated_of_is_sheaf

added theorem category_theory.presieve.is_sheaf_for.functor_inclusion_comp_extend

added theorem category_theory.presieve.is_sheaf_for.hom_ext

added theorem category_theory.presieve.is_sheaf_for.unique_extend

deleted theorem category_theory.presieve.is_sheaf_for_coarser_topology

modified theorem category_theory.presieve.is_sheaf_for_iff_generate

added theorem category_theory.presieve.is_sheaf_for_iff_yoneda_sheaf_condition

added theorem category_theory.presieve.is_sheaf_of_le

added theorem category_theory.presieve.is_sheaf_of_yoneda

deleted theorem category_theory.presieve.is_sheaf_yoneda

deleted theorem category_theory.presieve.separated_of_sheaf

deleted theorem category_theory.presieve.yoneda_condition_iff_sheaf_condition