Type of functions with locally finite support

This file defines functions with locally finite support, provides supporting API. For suitable targets, it establishes functions with locally finite support as an instance of a lattice ordered commutative group.

Throughout the present file, X denotes a topologically space and U a subset of X.

Definition, coercion to functions and basic extensionality lemmas

A function with locally finite support within U is a function X → Y whose support is locally finite within U and entirely contained in U. For T1-spaces, the theorem supportDiscreteWithin_iff_locallyFiniteWithin shows that the first condition is equivalent to the condition that the support f is discrete within U.

structure Function.locallyFinsuppWithin {X : Type u_1} [TopologicalSpace X] (U : Set X) (Y : Type u_2) [Zero Y] : Type (max u_1 u_2)

A function with locally finite support within U is a triple as specified below.

• toFun : X → Y

  A function X → Y

• supportWithinDomain' : Function.support self.toFun ⊆ U

  A proof that the support of toFun is contained in U

• supportLocallyFiniteWithinDomain' (z : X) : z ∈ U → ∃ t ∈ nhds z, (t ∩ Function.support self.toFun).Finite

  A proof the the support is locally finite within U

def Function.locallyFinsupp (X : Type u_1) [TopologicalSpace X] (Y : Type u_2) [Zero Y] : Type (max u_1 u_2)

A function with locally finite support is a function with locally finite support within ⊤ : Set X.

theorem supportDiscreteWithin_iff_locallyFiniteWithin {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [Zero Y] {f : X → Y} (h : 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.

instance Function.locallyFinsuppWithin.instFunLike {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] : FunLike (locallyFinsuppWithin U Y) X Y

Functions with locally finite support within U are FunLike: the coercion to functions is injective.

@[reducible, inline]

abbrev Function.locallyFinsuppWithin.support {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) : Set X

This allows writing D.support instead of Function.support D

theorem Function.locallyFinsuppWithin.supportWithinDomain {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) : D.support ⊆ U

theorem Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (D : locallyFinsuppWithin U Y) (z : X) : z ∈ U → ∃ t ∈ nhds z, (t ∩ D.support).Finite

theorem Function.locallyFinsuppWithin.ext {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} (h : ∀ (a : X), D₁ a = D₂ a) : D₁ = D₂

theorem Function.locallyFinsuppWithin.ext_iff {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ = D₂ ↔ ∀ (a : X), D₁ a = D₂ a

theorem Function.locallyFinsuppWithin.coe_injective {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] : Injective fun (x : locallyFinsuppWithin U Y) => ⇑x

Elementary properties of the support

@[simp]

theorem Function.locallyFinsuppWithin.apply_eq_zero_of_notMem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {z : X} (D : locallyFinsuppWithin U Y) (hz : z ∉ U) : D z = 0

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

@[deprecated Function.locallyFinsuppWithin.apply_eq_zero_of_notMem (since := "2025-05-23")]

theorem Function.locallyFinsuppWithin.apply_eq_zero_of_not_mem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {z : X} (D : locallyFinsuppWithin U Y) (hz : z ∉ U) : D z = 0

Alias of Function.locallyFinsuppWithin.apply_eq_zero_of_notMem.

---

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

theorem Function.locallyFinsuppWithin.eq_zero_codiscreteWithin {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] [T1Space X] (D : 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.

theorem Function.locallyFinsuppWithin.discreteSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] [T1Space X] (D : locallyFinsuppWithin U Y) : DiscreteTopology ↑D.support

On a T1 space, the support of a functions with locally finite support within U is discrete.

theorem Function.locallyFinsuppWithin.closedSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : 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.

theorem Function.locallyFinsuppWithin.finiteSupport {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [T2Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : IsCompact U) : D.support.Finite

If X is T2 and if U is compact, then the support of a function with locally finite support within U is finite.

Lattice ordered group structure

If X is a suitable instance, this section equips functions with locally finite support within U with the standard structure of a lattice ordered group, where addition, comparison, min and max are defined pointwise.

def Function.locallyFinsuppWithin.addSubgroup {X : Type u_1} [TopologicalSpace X] (U : Set X) {Y : Type u_2} [AddCommGroup Y] : AddSubgroup (X → Y)

Functions with locally finite support within U form an additive subgroup of functions X → Y.

theorem Function.locallyFinsuppWithin.memAddSubgroup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) : ⇑D ∈ locallyFinsuppWithin.addSubgroup U

def Function.locallyFinsuppWithin.mk_of_mem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) : locallyFinsuppWithin U Y

Assign a function with locally finite support within U to a function in the subgroup.

@[simp]

theorem Function.locallyFinsuppWithin.mk_of_mem_toFun {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) (a✝ : X) : (mk_of_mem f hf) a✝ = f a✝

instance Function.locallyFinsuppWithin.instZero {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Zero (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instAdd {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Add (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instNeg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Neg (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSub {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : Sub (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSMulNat {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : SMul ℕ (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instSMulInt {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.coe_zero {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : ⇑0 = 0

@[simp]

theorem Function.locallyFinsuppWithin.coe_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) : ⇑(D₁ + D₂) = ⇑D₁ + ⇑D₂

@[simp]

theorem Function.locallyFinsuppWithin.coe_neg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) : ⇑(-D) = -⇑D

@[simp]

theorem Function.locallyFinsuppWithin.coe_sub {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) : ⇑(D₁ - D₂) = ⇑D₁ - ⇑D₂

@[simp]

theorem Function.locallyFinsuppWithin.coe_nsmul {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℕ) : ⇑(n • D) = n • ⇑D

@[simp]

theorem Function.locallyFinsuppWithin.coe_zsmul {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) : ⇑(n • D) = n • ⇑D

instance Function.locallyFinsuppWithin.instAddCommGroup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] : AddCommGroup (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instLE {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [LE Y] [Zero Y] : LE (locallyFinsuppWithin U Y)

theorem Function.locallyFinsuppWithin.le_def {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [LE Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ ≤ D₂ ↔ ⇑D₁ ≤ ⇑D₂

instance Function.locallyFinsuppWithin.instLTOfPreorder {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Preorder Y] [Zero Y] : LT (locallyFinsuppWithin U Y)

theorem Function.locallyFinsuppWithin.lt_def {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Preorder Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ < D₂ ↔ ⇑D₁ < ⇑D₂

instance Function.locallyFinsuppWithin.instMaxOfSemilatticeSup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeSup Y] [Zero Y] : Max (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.max_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeSup Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} : (D₁ ⊔ D₂) x = D₁ x ⊔ D₂ x

instance Function.locallyFinsuppWithin.instMinOfSemilatticeInf {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeInf Y] [Zero Y] : Min (locallyFinsuppWithin U Y)

@[simp]

theorem Function.locallyFinsuppWithin.min_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [SemilatticeInf Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} : (D₁ ⊓ D₂) x = D₁ x ⊓ D₂ x

instance Function.locallyFinsuppWithin.instLattice {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [Zero Y] : Lattice (locallyFinsuppWithin U Y)

instance Function.locallyFinsuppWithin.instIsOrderedAddMonoid {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] : IsOrderedAddMonoid (locallyFinsuppWithin U Y)

Functions with locally finite support within U form an ordered commutative group.

Restriction

noncomputable def Function.locallyFinsuppWithin.restrict {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : 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.

theorem Function.locallyFinsuppWithin.restrict_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) (z : X) : (D.restrict h) z = if z ∈ V then D z else 0

theorem Function.locallyFinsuppWithin.restrict_eqOn {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) (⇑D) V

theorem Function.locallyFinsuppWithin.restrict_eqOn_compl {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) 0 Vᶜ

noncomputable def Function.locallyFinsuppWithin.restrictMonoidHom {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] {V : Set X} (h : V ⊆ U) : locallyFinsuppWithin U Y →+ locallyFinsuppWithin V Y

Restriction as a group morphism

@[simp]

theorem Function.locallyFinsuppWithin.restrictMonoidHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : (restrictMonoidHom h) D = D.restrict h

noncomputable def Function.locallyFinsuppWithin.restrictLatticeHom {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [Lattice Y] {V : Set X} (h : V ⊆ U) : LatticeHom (locallyFinsuppWithin U Y) (locallyFinsuppWithin V Y)

Restriction as a lattice morphism

@[simp]

theorem Function.locallyFinsuppWithin.restrictLatticeHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [Lattice Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : (restrictLatticeHom h) D = D.restrict h