X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), str X F ∈ s → IsOpen s → s ∈ ↑F
X : Compactum
F : Ultrafilter X.A
⊢ Ultrafilter.lim F = str X F
rw [Ultrafilter.lim_eq_iff_le_nhds, le_nhds_iff]
no goals
X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), str X F ∈ s → IsOpen s → s ∈ ↑F
tauto