Theorems · Definition · general topology

Function.locallyFinsuppWithin.restrict

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : Zero Y] → {V : Set X} → Function.locallyFinsuppWithin U Y → V ⊆ U → Function.locallyFinsuppWithin V Y

If V is a subset of U, then functions with locally finite support within U restrict to functions with locally finite support within V, by setting their values to zero outside of V.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceZero