Theorems · Theorem · general topology

Function.locallyFinsuppWithin.closedSupport

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [inst_2 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), IsClosed U → IsClosed D.support

If X is T1 and if U is closed, then the support of support of a function with locally finite support within U is also closed.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1SpaceZero