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

case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = S → IsClosed J₁ S
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S ↔ close J₁ S = S
constructor
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S = S
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S → close J₁ S = S
intro h
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S ≤ S

case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ S ≤ close J₁ S
case mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S = S
apply le_antisymm
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ S.arrows f
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S ≤ S
intro Y f hf
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ Covers J₁ S f
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ S.arrows f
rw [← J₁.covers_iff_mem_of_isClosed h]
no goals
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ Covers J₁ S f
apply hf
no goals
case mp.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ S ≤ close J₁ S
apply J₁.le_close
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ S
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = S → IsClosed J₁ S
intro e
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ (close J₁ S)
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ S
rw [← e]
no goals
case mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ (close J₁ S)
apply J₁.close_isClosed