Theorems · Theorem · general topology

AccPt.nhds_inter

∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} {x : α} {U : Set α},
  AccPt x (Filter.principal C) → U ∈ nhds x → AccPt x (Filter.principal (U ∩ C))

If x is an accumulation point of a set C and U is a neighborhood of x, then x is an accumulation point of U ∩ C.

Defined in

Mathlib.Topology.Perfect

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpace