no goals
α : Type u
β : Type v
ι : Type ?u.73726
π : ι → Type ?u.73731
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s t : Set α
inst✝¹ : CompactSpace α
f : Filter α
inst✝ : NeBot f
⊢ ∃ x, ClusterPt x f
simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)
no goals
α : Type u
β : Type v
ι : Type ?u.73726
π : ι → Type ?u.73731
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s t : Set α
inst✝¹ : CompactSpace α
f : Filter α
inst✝ : NeBot f
⊢ f ≤ 𝓟 univ
simp