Theorems · Theorem · general topology

Function.locallyFinsuppWithin.eq_zero_codiscreteWithin

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] [T1Space X]
  (D : Function.locallyFinsuppWithin U Y), ⇑D =ᶠ[Filter.codiscreteWithin U] 0

On a T1 space, the support of a function with locally finite support within U is discrete 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

TopologicalSpaceZeroT1Space