case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
⊢ ∀ (f : Y ⟶ X),
    (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X).toOrderHom S).arrows f
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
⊢ GrothendieckTopology.close (topologyOfClosureOperator c pb) S = ↑(c X).toOrderHom S
ext Y
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X).toOrderHom S).arrows f
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
⊢ ∀ (f : Y ⟶ X),
    (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X).toOrderHom S).arrows f
intro f
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ↑(c Y).toOrderHom (Sieve.pullback f S) = ⊤ ↔ (↑(c X).toOrderHom S).arrows f
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X).toOrderHom S).arrows f
change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f
no goals
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y).toOrderHom (Sieve.pullback f S) = Sieve.pullback f (↑(c X).toOrderHom S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ↑(c Y).toOrderHom (Sieve.pullback f S) = ⊤ ↔ (↑(c X).toOrderHom S).arrows f
rw [pb, Sieve.pullback_eq_top_iff_mem]