α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[{x}ᶜ] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ AccPt x (𝓟 (U ∩ C))
have : 𝓝[≠] x ≤ 𝓟 U := by
  rw [le_principal_iff]
  exact mem_nhdsWithin_of_mem_nhds hU
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[{x}ᶜ] x ≤ 𝓟 U
⊢ NeBot (𝓝[{x}ᶜ] x ⊓ 𝓟 C)
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[{x}ᶜ] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))
rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]
no goals
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[{x}ᶜ] x ≤ 𝓟 U
⊢ NeBot (𝓝[{x}ᶜ] x ⊓ 𝓟 C)
exact h_acc
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[{x}ᶜ] x
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ 𝓝[{x}ᶜ] x ≤ 𝓟 U
rw [le_principal_iff]
no goals
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[{x}ᶜ] x
exact mem_nhdsWithin_of_mem_nhds hU