C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ sieves J Y
C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ Covers J S f
rw [Covers, (Sieve.pullback_eq_top_iff_mem f).1 hf]
no goals
C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ sieves J Y
apply J.top_mem