X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), Compactum.cl A ∈ F → str X F ∈ Compactum.cl A
X : Compactum
A : Set X.A
⊢ IsClosed (Compactum.cl A)
rw [isClosed_iff]
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : Compactum.cl A ∈ F
⊢ str X F ∈ Compactum.cl A
X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), Compactum.cl A ∈ F → str X F ∈ Compactum.cl A
intro F hF
no goals
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : Compactum.cl A ∈ F
⊢ str X F ∈ Compactum.cl A
exact cl_cl _ ⟨F, hF, rfl⟩