case intro.intro
α : Type u
β : Type v
ι : Type ?u.150954
π : ι → Type ?u.150959
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
F : Ultrafilter α
x : α
h : ↑F ≤ 𝓝 x
⊢ ↑F ≤ 𝓝 (lim F)
α : Type u
β : Type v
ι : Type ?u.150954
π : ι → Type ?u.150959
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
F : Ultrafilter α
⊢ ↑F ≤ 𝓝 (lim F)
rcases isCompact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.150954
π : ι → Type ?u.150959
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
F : Ultrafilter α
x : α
h : ↑F ≤ 𝓝 x
⊢ ↑F ≤ 𝓝 (lim F)
exact le_nhds_lim ⟨x, h⟩
no goals
α : Type u
β : Type v
ι : Type ?u.150954
π : ι → Type ?u.150959
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
F : Ultrafilter α
⊢ ↑F ≤ 𝓟 univ
simp