α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
refine' ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => _⟩
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
haveI := hl.1
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
x : α
hxs : x ∈ s
hxl : ↑(Ultrafilter.of l) ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
x : α
hxs : x ∈ s
hxl : ↑(Ultrafilter.of l) ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ ClusterPt x l
exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩