Theorems · Theorem · category theory

CategoryTheory.Precoverage.generate_mem_toGrothendieck

∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} {X : C}
  {R : CategoryTheory.Presieve X}, R ∈ J.coverings X → CategoryTheory.Sieve.generate R ∈ J.toGrothendieck X

Defined in

Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Cited by

12 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category