Theorems · Theorem · general topology

supportDiscreteWithin_iff_locallyFiniteWithin

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [inst_2 : Zero Y] {f : X → Y},
  Function.support f ⊆ U → (f =ᶠ[Filter.codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite)

For T1 spaces, the condition supportLocallyFiniteWithinDomain' is equivalent to saying that the support is codiscrete within U.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1SpaceZero