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 that the support is locally finite within U

@[reducible, inline]

abbrev 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.

Equations

• Function.locallyFinsupp X Y = Function.locallyFinsuppWithin Set.univ Y

@[instance_reducible]

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

Function with locally finite support have a zero.

Equations

• instZeroLocallyFinsuppWithin = { zero := { toFun := fun (x : X) => 0, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ } }

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.

def LocallyFiniteSupport {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] (f : X → Y) : Prop

A function f : X → Y has locally finite support if for every z : X, there is a neighbourhood t around z such that t ∩ f.support is finite.

Equations

• LocallyFiniteSupport f = ∀ (z : X), ∃ t ∈ nhds z, (t ∩ Function.support f).Finite

theorem LocallyFiniteSupport.iff_locallyFinite_support {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] (f : X → Y) : (LocallyFinite fun (s : ↑(Function.support f)) => {↑s}) ↔ LocallyFiniteSupport f

theorem LocallyFiniteSupport.locallyFinite_support {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] (f : X → Y) (h : LocallyFiniteSupport f) : LocallyFinite fun (s : ↑(Function.support f)) => {↑s}

theorem LocallyFiniteSupport.finite_inter_support_of_isCompact {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} {W : Set X} [Zero Y] {f : X → Y} (h : LocallyFiniteSupport f) (hW : IsCompact W) : (W ∩ Function.support f).Finite

theorem Function.locallyFinsupp.locallyFiniteSupport {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] (f : locallyFinsupp X Y) : LocallyFiniteSupport f.toFun

@[instance_reducible, macro_inline]

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.

Equations

• Function.locallyFinsuppWithin.instFunLike = { coe := fun (D : Function.locallyFinsuppWithin U Y) => D.toFun, coe_injective := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.toFun_eq_coe {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (c : locallyFinsuppWithin U Y) : c.toFun = ⇑c

@[simp]

theorem Function.locallyFinsuppWithin.coe_mk {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (f : X → Y) (h : Function.support f ⊆ U) (h' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite) : ⇑{ toFun := f, supportWithinDomain' := h, supportLocallyFiniteWithinDomain' := h' } = f

@[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

Equations

• D.support = 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.locallyFinsupp.finite_support {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] [CompactSpace X] (f : locallyFinsupp X Y) : (locallyFinsuppWithin.support f).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

Singleton Indicators as Functions with Locally Finite Support

noncomputable def Function.locallyFinsuppWithin.single {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] (x : X) (y : Y) : locallyFinsupp X Y

Is analogy to Finsupp.single, this definition presents the indicator function of a single point as a function with locally finite support.

Equations

• Function.locallyFinsuppWithin.single x y = { toFun := Pi.single x y, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.single_apply {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] {x₁ x₂ : X} {y : Y} : (single x₁ y) x₂ = if x₂ = x₁ then y else 0

Simplifier lemma: single x y takes the value y at x and is zero otherwise.

@[simp]

theorem Function.locallyFinsuppWithin.single_zero {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] {x : X} : single x 0 = 0

Simplifier lemma: single x 0 is zero.

@[simp]

theorem Function.locallyFinsuppWithin.coe_single {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] {x : X} {y : Y} : ⇑(single x y) = Pi.single x y

Simplifier lemma: coercion of single x y to a function.

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.

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) : IsDiscrete D.support

On a T1 space, the support of a function 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.addSubmonoid {X : Type u_1} [TopologicalSpace X] (U : Set X) {Y : Type u_2} [AddMonoid Y] : AddSubmonoid (X → Y)

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

Equations

• Function.locallyFinsuppWithin.addSubmonoid U = { carrier := {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem Function.locallyFinsuppWithin.memAddSubmonoid {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddMonoid Y] (D : locallyFinsuppWithin U Y) : ⇑D ∈ locallyFinsuppWithin.addSubmonoid U

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

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

Equations

• One or more equations did not get rendered due to their size.

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

def Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) : locallyFinsuppWithin U Y

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

Equations

• Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid f hf = { toFun := f, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid_toFun {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) (a✝ : X) : (mk_of_mem_addSubmonoid f hf) a✝ = f a✝

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instAdd = { add := fun (D₁ D₂ : Function.locallyFinsuppWithin U Y) => Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid (⇑D₁ + ⇑D₂) ⋯ }

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instSMulNat = { smul := fun (n : ℕ) (D : Function.locallyFinsuppWithin U Y) => Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid (n • ⇑D) ⋯ }

def Function.locallyFinsuppWithin.mk_of_mem_addSubgroup {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddGroup 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.

Equations

• Function.locallyFinsuppWithin.mk_of_mem_addSubgroup f hf = { toFun := f, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

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

@[deprecated Function.locallyFinsuppWithin.mk_of_mem_addSubgroup (since := "2026-03-06")]

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

Alias of Function.locallyFinsuppWithin.mk_of_mem_addSubgroup.

---

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

Equations

• @Function.locallyFinsuppWithin.mk_of_mem = @Function.locallyFinsuppWithin.mk_of_mem_addSubgroup

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instNeg = { neg := fun (D : Function.locallyFinsuppWithin U Y) => Function.locallyFinsuppWithin.mk_of_mem_addSubgroup (-⇑D) ⋯ }

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instSub = { sub := fun (D₁ D₂ : Function.locallyFinsuppWithin U Y) => Function.locallyFinsuppWithin.mk_of_mem_addSubgroup (⇑D₁ - ⇑D₂) ⋯ }

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instSMulInt = { smul := fun (n : ℤ) (D : Function.locallyFinsuppWithin U Y) => Function.locallyFinsuppWithin.mk_of_mem_addSubgroup (n • ⇑D) ⋯ }

@[simp]

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

@[simp]

theorem Function.locallyFinsuppWithin.coe_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddMonoid 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} [AddGroup 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} [AddGroup 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} [AddMonoid 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} [AddGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) : ⇑(n • D) = n • ⇑D

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instAddMonoid = Function.Injective.addMonoid (fun (x : Function.locallyFinsuppWithin U Y) => ⇑x) ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instAddCommMonoid = Function.Injective.addCommMonoid (fun (x : Function.locallyFinsuppWithin U Y) => ⇑x) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Function.locallyFinsuppWithin.coe_sum {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommMonoid Y] {ι : Type u_3} {s : Finset ι} {F : ι → locallyFinsuppWithin U Y} : ⇑(∑ n ∈ s, F n) = ∑ n ∈ s, ⇑(F n)

@[simp]

theorem Function.locallyFinsuppWithin.coe_finsum {X : Type u_1} [TopologicalSpace X] {U : Set X} {ι : Type u_3} {F : ι → locallyFinsuppWithin U ℤ} : ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instAddGroup = Function.Injective.addGroup (fun (x : Function.locallyFinsuppWithin U Y) => ⇑x) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Function.locallyFinsuppWithin.support_neg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddGroup Y] (D : locallyFinsuppWithin U Y) : (-D).support = D.support

Simplifier lemma: Support does not change when replacing a function with locally finite support by its negative.

@[instance_reducible]

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

Equations

• Function.locallyFinsuppWithin.instAddCommGroup = Function.Injective.addCommGroup (fun (x : Function.locallyFinsuppWithin U Y) => ⇑x) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Function.locallyFinsuppWithin.supported {X : Type u_1} [TopologicalSpace X] (Y : Type u_2) [AddGroup Y] (U s : Set X) : AddSubgroup (locallyFinsuppWithin U Y)

supported Y U s is the additive subgroup of those functions with locally finite support within U whose support is contained in s.

This is the analogue of Finsupp.supported, which cannot be used here: it is a Submodule of α →₀ M and so requires a semiring acting on a commutative M, whereas Y is an arbitrary additive group.

Equations

• Function.locallyFinsuppWithin.supported Y U s = { carrier := {D : Function.locallyFinsuppWithin U Y | D.support ⊆ s}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.mem_supported {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddGroup Y] {s : Set X} {D : locallyFinsuppWithin U Y} : D ∈ supported Y U s ↔ D.support ⊆ s

@[instance_reducible]

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)

Equations

• Function.locallyFinsuppWithin.instLE = { le := fun (D₁ D₂ : Function.locallyFinsuppWithin U Y) => ⇑D₁ ≤ ⇑D₂ }

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₂

theorem Function.locallyFinsuppWithin.single_nonneg {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] [Preorder Y] {x : X} {y : Y} : 0 ≤ single x y ↔ 0 ≤ y

@[instance_reducible]

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)

Equations

• Function.locallyFinsuppWithin.instLTOfPreorder = { lt := fun (D₁ D₂ : Function.locallyFinsuppWithin U Y) => ⇑D₁ < ⇑D₂ }

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₂

theorem Function.locallyFinsuppWithin.single_pos {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [Zero Y] [Preorder Y] {x : X} {y : Y} : 0 < single x y ↔ 0 < y

@[simp]

theorem Function.locallyFinsuppWithin.single_pos_nat_one {X : Type u_1} [TopologicalSpace X] [DecidableEq X] {x : X} : 0 < single x 1

@[simp]

theorem Function.locallyFinsuppWithin.single_pos_int_one {X : Type u_1} [TopologicalSpace X] [DecidableEq X] {x : X} : 0 < single x 1

@[instance_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[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_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[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_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Function.locallyFinsuppWithin.posPart_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [AddCommGroup Y] (a : locallyFinsuppWithin U Y) (x : X) : a⁺ x = (a x)⁺

@[simp]

theorem Function.locallyFinsuppWithin.negPart_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Lattice Y] [AddCommGroup Y] (a : locallyFinsuppWithin U Y) (x : X) : a⁻ x = (a x)⁻

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.

theorem Function.locallyFinsuppWithin.posPart_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : locallyFinsuppWithin U Y) : (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺

The positive part of a sum is less than or equal to the sum of the positive parts.

theorem Function.locallyFinsuppWithin.negPart_add {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : locallyFinsuppWithin U Y) : (f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻

The negative part of a sum is less than or equal to the sum of the negative parts.

@[simp]

theorem Function.locallyFinsuppWithin.nsmul_posPart {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : locallyFinsuppWithin U Y) : (n • f)⁺ = n • f⁺

Taking the positive part of a function with locally finite support commutes with scalar multiplication by a natural number.

@[simp]

theorem Function.locallyFinsuppWithin.nsmul_negPart {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : locallyFinsuppWithin U Y) : (n • f)⁻ = n • f⁻

Taking the negative part of a function with locally finite support commutes with scalar multiplication by a natural number.

theorem Function.locallyFinsuppWithin.exists_single_le_pos {X : Type u_1} [TopologicalSpace X] [DecidableEq X] {D : locallyFinsupp X ℤ} (h : 0 < D) : ∃ (e : X), single e 1 ≤ D

Every positive function with locally finite supports dominates a singleton indicator.

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.

Equations

• D.restrict h = { toFun := fun (z : X) => if hz : z ∈ V then D z else 0, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

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ᶜ

@[simp]

theorem Function.locallyFinsuppWithin.restrict_zero {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] {U V : Set X} (hV : V ⊆ U) : restrict 0 hV = 0

Restriction of the zero function is the zero function.

theorem Function.locallyFinsuppWithin.restrict_mono {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] [LinearOrder Y] {A B : locallyFinsuppWithin U Y} {V : Set X} (hVU : V ⊆ U) (hAB : A ≤ B) : A.restrict hVU ≤ B.restrict hVU

Restriction is monotone

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

Equations

• Function.locallyFinsuppWithin.restrictMonoidHom h = { toFun := fun (D : Function.locallyFinsuppWithin U Y) => D.restrict h, map_zero' := ⋯, map_add' := ⋯ }

@[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.restrictOrderMonoidHom {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [AddCommGroup Y] [LinearOrder Y] {V : Set X} (h : V ⊆ U) : locallyFinsuppWithin U Y →+o locallyFinsuppWithin V Y

Restriction as an ordered group morphism

Equations

• Function.locallyFinsuppWithin.restrictOrderMonoidHom h = { toFun := fun (D : Function.locallyFinsuppWithin U Y) => D.restrict h, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

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

@[simp]

theorem Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [DecidableEq X] [AddCommMonoid Y] {U : Set X} {F : locallyFinsuppWithin U Y} (h : F.support.Finite) : ∑ᶠ (x : X), restrict (single x (F x)) ⋯ = F

Present a function with with finite support as a finsum of singleton indicator functions.

@[simp]

theorem Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self_on_univ {X : Type u_1} [TopologicalSpace X] [DecidableEq X] {D : locallyFinsupp X ℤ} (h : (support D).Finite) : ∑ z ∈ h.toFinset, single z (D z) = D

Represent a function (of locally finite support) that in fact has finite support as a finsum of singleton indicator functions.

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

Equations

• Function.locallyFinsuppWithin.restrictLatticeHom h = { toFun := fun (D : Function.locallyFinsuppWithin U Y) => D.restrict h, map_sup' := ⋯, map_inf' := ⋯ }

@[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

theorem Function.locallyFinsuppWithin.restrict_posPart {X : Type u_1} [TopologicalSpace X] {U V : Set X} (D : locallyFinsuppWithin U ℤ) (h : V ⊆ U) : D⁺.restrict h = (D.restrict h)⁺

Restriction commutes with taking positive parts.

theorem Function.locallyFinsuppWithin.restrict_negPart {X : Type u_1} [TopologicalSpace X] {U V : Set X} (D : locallyFinsuppWithin U ℤ) (h : V ⊆ U) : D⁻.restrict h = (D.restrict h)⁻

Restriction commutes with taking negative parts.

theorem Function.locallyFinsuppWithin.disjoint_nhdsWithin_cofinite_of_mem {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_2} [Zero Y] (f : locallyFinsuppWithin U Y) (p : X) (hp : p ∈ U) : Disjoint (nhdsWithin p f.support) Filter.cofinite

theorem Function.locallyFinsupp.disjoint_nhdsWithin_cofinite {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [Zero Y] (f : locallyFinsupp X Y) (p : X) : Disjoint (nhdsWithin p (locallyFinsuppWithin.support f)) Filter.cofinite

Composition a.k.a. mapRange

See the documentation of Finsupp.mapRange for further explanation and a list of similar definitions.

def Function.locallyFinsuppWithin.mapRange {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} {Z : Type u_4} [Zero Y] [Zero Z] (f : Y → Z) (hf : f 0 = 0) (g : locallyFinsuppWithin U Y) : locallyFinsuppWithin U Z

The composition of f : Y → Z and g : locallyFinsuppWithin is mapRange f hf g : locallyFinsuppWithin, which is well-defined when f 0 = 0.

Equations

• Function.locallyFinsuppWithin.mapRange f hf g = { toFun := f ∘ ⇑g, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.mapRange_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} {Z : Type u_4} [Zero Y] [Zero Z] {f : Y → Z} {hf : f 0 = 0} {g : locallyFinsuppWithin U Y} {a : X} : (mapRange f hf g) a = f (g a)

theorem Function.locallyFinsuppWithin.support_mapRange_subset {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} {Z : Type u_4} [Zero Y] [Zero Z] (f : Y → Z) (hf : f 0 = 0) (g : locallyFinsuppWithin U Y) : (mapRange f hf g).support ⊆ g.support

Truncation of a Function with Locally Finite Support

@[reducible, inline]

noncomputable abbrev Function.locallyFinsuppWithin.truncate {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y : Y) (hy : 0 ≤ y) : locallyFinsuppWithin U Y

Truncation of a function with locally finite support: the pointwise minimum with a non-negative constant y.

Equations

• D.truncate y hy = Function.locallyFinsuppWithin.mapRange (fun (x : Y) => min x y) ⋯ D

@[reducible, inline]

noncomputable abbrev Function.locallyFinsuppWithin.truncate₁ {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] [One Y] [ZeroLEOneClass Y] (D : locallyFinsuppWithin U Y) : locallyFinsuppWithin U Y

Truncation of a function with locally finite support: the pointwise minimum with the constant 1.

This is an abbrev for D.truncate 1 zero_le_one, so all lemmas about truncate apply directly. For instance, D.truncate_le 1 _ : D.truncate₁ ≤ D, where Lean infers the proof of 0 ≤ 1 from the expected type.

Equations

• D.truncate₁ = D.truncate 1 ⋯

@[simp]

theorem Function.locallyFinsuppWithin.truncate_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y : Y) (hy : 0 ≤ y) (z : X) : (D.truncate y hy) z = min (D z) y

Evaluation of the truncation.

@[simp]

theorem Function.locallyFinsuppWithin.truncate_zero {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} {y : Y} [Zero Y] [LinearOrder Y] {hy : 0 ≤ y} : truncate 0 y hy = 0

Truncation of the zero function.

theorem Function.locallyFinsuppWithin.truncate_le {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y : Y) (hy : 0 ≤ y) : D.truncate y hy ≤ D

Truncation decreases functions.

theorem Function.locallyFinsuppWithin.truncate_mono {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] {D₁ D₂ : locallyFinsuppWithin U Y} (y : Y) (hy : 0 ≤ y) (h : D₁ ≤ D₂) : D₁.truncate y hy ≤ D₂.truncate y hy

Truncation is monotone.

theorem Function.locallyFinsuppWithin.truncate_nonneg {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] {D : locallyFinsuppWithin U Y} (y : Y) (hy : 0 ≤ y) (h : 0 ≤ D) : 0 ≤ D.truncate y hy

Truncation preserves non-negativity.

@[simp]

theorem Function.locallyFinsuppWithin.truncate_truncate {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y₁ y₂ : Y) (hy₁ : 0 ≤ y₁) (hy₂ : 0 ≤ y₂) : (D.truncate y₁ hy₁).truncate y₂ hy₂ = D.truncate (min y₁ y₂) ⋯

Repeated truncation is truncation at minimum.

theorem Function.locallyFinsuppWithin.truncate_idempotent {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y : Y) (hy : 0 ≤ y) : (D.truncate y hy).truncate y hy = D.truncate y hy

Truncation is idempotent.

theorem Function.locallyFinsuppWithin.support_truncate {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (D : locallyFinsuppWithin U Y) (y : Y) (hy : 0 < y) : (D.truncate y ⋯).support = D.support

Truncation does not change the support.

noncomputable def Function.locallyFinsuppWithin.truncateOrderHom {X : Type u_1} [TopologicalSpace X] (U : Set X) {Y : Type u_3} [Zero Y] [LinearOrder Y] (y : Y) (hy : 0 ≤ y) : locallyFinsuppWithin U Y →o locallyFinsuppWithin U Y

Truncation as an order homomorphism.

Equations

• Function.locallyFinsuppWithin.truncateOrderHom U y hy = { toFun := fun (D : Function.locallyFinsuppWithin U Y) => D.truncate y hy, monotone' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.truncateOrderHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (y : Y) (hy : 0 ≤ y) (D : locallyFinsuppWithin U Y) : (truncateOrderHom U y hy) D = D.truncate y hy

Evaluation of the order homomorphism truncateOrderHom.

noncomputable def Function.locallyFinsuppWithin.truncateLatticeHom {X : Type u_1} [TopologicalSpace X] (U : Set X) {Y : Type u_3} [Zero Y] [LinearOrder Y] (y : Y) (hy : 0 ≤ y) : LatticeHom (locallyFinsuppWithin U Y) (locallyFinsuppWithin U Y)

Truncation as a lattice homomorphism.

Equations

• Function.locallyFinsuppWithin.truncateLatticeHom U y hy = { toFun := fun (D : Function.locallyFinsuppWithin U Y) => D.truncate y hy, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem Function.locallyFinsuppWithin.truncateLatticeHom_apply {X : Type u_1} [TopologicalSpace X] {U : Set X} {Y : Type u_3} [Zero Y] [LinearOrder Y] (y : Y) (hy : 0 ≤ y) (D : locallyFinsuppWithin U Y) : (truncateLatticeHom U y hy) D = D.truncate y hy

Evaluation of the lattice homomorphism truncateLatticeHom.