α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
⊢ a ∈ s
let f := 𝓝[s] a
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
rcases h f this inf_le_right with ⟨y, ys, fy⟩
no goals
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]