X : Compactum
S : Set X.A
⊢ IsOpen (Sᶜ) ↔ ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
rw [← isOpen_compl_iff]
case mp
X : Compactum
S : Set X.A
⊢ IsOpen (Sᶜ) → ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S

case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S) → IsOpen (Sᶜ)
X : Compactum
S : Set X.A
⊢ IsOpen (Sᶜ) ↔ ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
constructor
case mp
X : Compactum
S : Set X.A
cond : IsOpen (Sᶜ)
F : Ultrafilter X.A
h : S ∈ F
⊢ str X F ∈ S
case mp
X : Compactum
S : Set X.A
⊢ IsOpen (Sᶜ) → ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
intro cond F h
case mp
X : Compactum
S : Set X.A
cond : IsOpen (Sᶜ)
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
⊢ False
case mp
X : Compactum
S : Set X.A
cond : IsOpen (Sᶜ)
F : Ultrafilter X.A
h : S ∈ F
⊢ str X F ∈ S
by_contra c
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
cond : Sᶜ ∈ F
⊢ False
case mp
X : Compactum
S : Set X.A
cond : IsOpen (Sᶜ)
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
⊢ False
specialize cond F c
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
cond : ¬S ∈ F
⊢ False
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
cond : Sᶜ ∈ F
⊢ False
rw [compl_mem_iff_not_mem] at cond
no goals
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : ¬str X F ∈ S
cond : ¬S ∈ F
⊢ False
contradiction
case mpr
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
⊢ Sᶜ ∈ F
case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S) → IsOpen (Sᶜ)
intro h1 F h2
case mpr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
⊢ Sᶜ ∈ F
case mpr
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → str X F ∈ S
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
⊢ Sᶜ ∈ F
specialize h1 F
case mpr.inl
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

case mpr.inr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F
case mpr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
⊢ Sᶜ ∈ F
cases' F.mem_or_compl_mem S with h h
no goals
case mpr.inl
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

case mpr.inr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : str X F ∈ Sᶜ
h1 : S ∈ F → str X F ∈ S
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F
exacts [absurd (h1 h) h2, h]