case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
⊢ Preperfect (U ∩ C)
rintro x ⟨xU, xC⟩
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))
apply (hC _ xC).nhds_inter
no goals
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x
exact hU.mem_nhds xU