X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
X : TopCat
ι : Type v
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCovering U) ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
intro x hx
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx
no goals
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩