case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ → S ∈ sieves J₁ X

case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ sieves J₁ X → close J₁ S = ⊤
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ ↔ S ∈ sieves J₁ X
constructor
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ S ∈ sieves J₁ X
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ → S ∈ sieves J₁ X
intro h
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ sieves J₁ Y
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ S ∈ sieves J₁ X
apply J₁.transitive (J₁.top_mem X)
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ Sieve.pullback f S ∈ sieves J₁ Y
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ sieves J₁ Y
intro Y f hf
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ (close J₁ S).arrows f
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ Sieve.pullback f S ∈ sieves J₁ Y
change J₁.close S f
no goals
case mp.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ (close J₁ S).arrows f
rwa [h]
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ close J₁ S = ⊤
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ sieves J₁ X → close J₁ S = ⊤
intro hS
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ ⊤ ≤ close J₁ S
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ close J₁ S = ⊤
rw [eq_top_iff]
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : ⊤.arrows f
⊢ (close J₁ S).arrows f
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ ⊤ ≤ close J₁ S
intro Y f _
no goals
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : ⊤.arrows f
⊢ (close J₁ S).arrows f
apply J₁.pullback_stable _ hS