Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 06:18 6fc35175

View on Github →

feat(category_theory/sites): generate lemmas (#4840) A couple of simple lemmas about the sieve generated by certain presieves.

Estimated changes

Modified src/category_theory/sites/pretopology.lean

Modified src/category_theory/sites/sieves.lean

added theorem category_theory.sieve.generate_of_contains_split_epi

added theorem category_theory.sieve.generate_of_singleton_split_epi

added theorem category_theory.sieve.generate_top

added theorem category_theory.sieve.le_generate