Theorems · Theorem · general topology

codiscreteWithin_iff_locallyEmptyComplementWithin

∀ {X : Type u_1} [inst : TopologicalSpace X] {s U : Set X},
  s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhdsWithin z {z}ᶜ, t ∩ (U \ s) = ∅

Helper lemma for codiscreteWithin_iff_locallyFiniteComplementWithin: A set s is codiscreteWithin U iff every point z ∈ U has a punctured neighborhood that does not intersect U \ s.

Defined in

Mathlib.Topology.DiscreteSubset

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace