Theorems · Theorem · general topology

codiscreteWithin_iff_locallyFiniteComplementWithin

∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s U : Set X},
  s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ (U \ s)).Finite

In a T1Space, a set s is codiscreteWithin U iff it has locally finite complement within U. More precisely: s is codiscreteWithin U iff every point z ∈ U has a punctured neighborhood intersect U \ s in only finitely many points.

Defined in

Mathlib.Topology.DiscreteSubset

Cited by

3 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT1Space