C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), sieveOfSection G s ∈ sieves J U.unop → s ∈ obj G U
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J (toPresheaf G) ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), sieveOfSection G s ∈ sieves J U.unop → s ∈ obj G U
rw [← G.eq_sheafify_iff h]
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), sieveOfSection G s ∈ sieves J U.unop → s ∈ obj G U
change _ ↔ G.sheafify J ≤ G
no goals
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G
exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩