C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ sieves J Y
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ R ⊓ S ∈ sieves J X
apply J.transitive rj _ fun Y f Hf => _
C : Type u
inst✝ : Category C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ sieves J Y
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ sieves J Y
intros Y f hf
C : Type u
inst✝ : Category C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ sieves J Y
C : Type u
inst✝ : Category C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ sieves J Y
rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]
no goals
C : Type u
inst✝ : Category C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ sieves J Y
simp [sj]