Theorems · Theorem · general topology

Function.locallyFinsuppWithin.apply_eq_zero_of_notMem

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {z : X}
  (D : Function.locallyFinsuppWithin U Y), z ∉ U → D z = 0

Simplifier lemma: Functions with locally finite support within U evaluate to zero outside of U.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

25 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceZero