α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f : Filter α
inst✝ : CompactSpace α
U : Set α
⊢ (∀ (x : α), x ∈ U → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f : Filter α
inst✝ : CompactSpace α
U : Set α
⊢ IsOpen U ↔ ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
rw [isOpen_iff_ultrafilter]
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f : Filter α
inst✝ : CompactSpace α
U : Set α
⊢ (∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F) → ∀ (x : α), x ∈ U → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → U ∈ l
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f : Filter α
inst✝ : CompactSpace α
U : Set α
⊢ (∀ (x : α), x ∈ U → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
refine' ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, _⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ : Filter α
inst✝ : CompactSpace α
U : Set α
cond : ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
x : α
hx : x ∈ U
f : Ultrafilter α
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f : Filter α
inst✝ : CompactSpace α
U : Set α
⊢ (∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F) → ∀ (x : α), x ∈ U → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → U ∈ l
intro cond x hx f h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ : Filter α
inst✝ : CompactSpace α
U : Set α
cond : ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
x : α
f : Ultrafilter α
hx : Ultrafilter.lim f ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ : Filter α
inst✝ : CompactSpace α
U : Set α
cond : ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
x : α
hx : x ∈ U
f : Ultrafilter α
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ : Filter α
inst✝ : CompactSpace α
U : Set α
cond : ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F
x : α
f : Ultrafilter α
hx : Ultrafilter.lim f ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
exact cond _ hx