# The topological support of a function #

In this file we define the topological support of a function f, tsupport f, as the closure of the support of f.

Furthermore, we say that f has compact support if the topological support of f is compact.

## Main definitions #

• mulTSupport & tsupport
• HasCompactMulSupport & HasCompactSupport

## Implementation Notes #

• We write all lemmas for multiplicative functions, and use @[to_additive] to get the more common additive versions.
• We do not put the definitions in the Function namespace, following many other topological definitions that are in the root namespace (compare Embedding vs Function.Embedding).
def tsupport {X : Type u_1} {α : Type u_2} [Zero α] [] (f : Xα) :
Set X

The topological support of a function is the closure of its support. i.e. the closure of the set of all elements where the function is nonzero.

Equations
Instances For
def mulTSupport {X : Type u_1} {α : Type u_2} [One α] [] (f : Xα) :
Set X

The topological support of a function is the closure of its support, i.e. the closure of the set of all elements where the function is not equal to 1.

Equations
Instances For
theorem subset_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [] (f : Xα) :
theorem subset_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [] (f : Xα) :
theorem isClosed_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [] (f : Xα) :
theorem isClosed_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [] (f : Xα) :
theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [Zero α] [] {f : Xα} :
f = 0
theorem mulTSupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [One α] [] {f : Xα} :
f = 1
theorem image_eq_zero_of_nmem_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [] {f : Xα} {x : X} (hx : x) :
f x = 0
theorem image_eq_one_of_nmem_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [] {f : Xα} {x : X} (hx : x) :
f x = 1
theorem range_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [] (f : Xα) :
insert 0 (f '' )
theorem range_subset_insert_image_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [] (f : Xα) :
insert 1 ()
theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [Zero α] [] (f : Xα) :
= f '' = insert 0 (f '' )
theorem range_eq_image_mulTSupport_or {X : Type u_1} {α : Type u_2} [One α] [] (f : Xα) :
= = insert 1 ()
theorem tsupport_mul_subset_left {X : Type u_1} [] {α : Type u_10} [] {f : Xα} {g : Xα} :
(tsupport fun (x : X) => f x * g x)
theorem tsupport_mul_subset_right {X : Type u_1} [] {α : Type u_10} [] {f : Xα} {g : Xα} :
(tsupport fun (x : X) => f x * g x)
theorem tsupport_smul_subset_left {X : Type u_1} {M : Type u_10} {α : Type u_11} [] [Zero M] [Zero α] [] (f : XM) (g : Xα) :
(tsupport fun (x : X) => f x g x)
theorem tsupport_smul_subset_right {X : Type u_1} {M : Type u_10} {α : Type u_11} [] [Zero α] [] (f : XM) (g : Xα) :
(tsupport fun (x : X) => f x g x)
theorem tsupport_add {X : Type u_1} {α : Type u_2} [] [] {f : Xα} {g : Xα} :
(tsupport fun (x : X) => f x + g x)
theorem mulTSupport_mul {X : Type u_1} {α : Type u_2} [] [] {f : Xα} {g : Xα} :
(mulTSupport fun (x : X) => f x * g x)
theorem not_mem_tsupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} {x : α} :
x (nhds x).EventuallyEq f 0
theorem not_mem_mulTSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} {x : α} :
x (nhds x).EventuallyEq f 1
theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [] [Zero β] [] {f : αβ} (hf : x, ) :
theorem continuous_of_mulTSupport {α : Type u_2} {β : Type u_4} [] [One β] [] {f : αβ} (hf : x, ) :

## Functions with compact support #

def HasCompactSupport {α : Type u_2} {β : Type u_4} [] [Zero β] (f : αβ) :

A function f has compact support or is compactly supported if the closure of the support of f is compact. In a T₂ space this is equivalent to f being equal to 0 outside a compact set.

Equations
Instances For
def HasCompactMulSupport {α : Type u_2} {β : Type u_4} [] [One β] (f : αβ) :

A function f has compact multiplicative support or is compactly supported if the closure of the multiplicative support of f is compact. In a T₂ space this is equivalent to f being equal to 1 outside a compact set.

Equations
Instances For
theorem hasCompactSupport_def {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} :
theorem hasCompactMulSupport_def {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} :
theorem exists_compact_iff_hasCompactSupport {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] :
(∃ (K : Set α), xK, f x = 0)
theorem exists_compact_iff_hasCompactMulSupport {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] :
(∃ (K : Set α), xK, f x = 1)
theorem HasCompactSupport.intro {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] {K : Set α} (hK : ) (hfK : xK, f x = 0) :
theorem HasCompactMulSupport.intro {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] {K : Set α} (hK : ) (hfK : xK, f x = 1) :
theorem HasCompactSupport.intro' {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} {K : Set α} (hK : ) (h'K : ) (hfK : xK, f x = 0) :
theorem HasCompactMulSupport.intro' {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} {K : Set α} (hK : ) (h'K : ) (hfK : xK, f x = 1) :
theorem HasCompactSupport.of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] {K : Set α} (hK : ) (h : ) :
theorem HasCompactMulSupport.of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] {K : Set α} (hK : ) (h : ) :
theorem HasCompactSupport.isCompact {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} (hf : ) :
theorem HasCompactMulSupport.isCompact {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} (hf : ) :
theorem hasCompactSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} :
.EventuallyEq f 0
theorem hasCompactMulSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} :
.EventuallyEq f 1
theorem isCompact_range_of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] (hf : ) {k : Set α} (hk : ) (h'f : ) :
theorem isCompact_range_of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] (hf : ) {k : Set α} (hk : ) (h'f : ) :
theorem HasCompactSupport.isCompact_range {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] (h : ) (hf : ) :
theorem HasCompactMulSupport.isCompact_range {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] (h : ) (hf : ) :
theorem HasCompactSupport.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [Zero β] [Zero γ] {f : αβ} {f' : αγ} (hf : ) (hff' : ) :
theorem HasCompactMulSupport.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [One β] [One γ] {f : αβ} {f' : αγ} (hf : ) (hff' : ) :
theorem HasCompactSupport.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [Zero β] [Zero γ] {f : αβ} {f' : αγ} (hf : ) (hff' : ) :
theorem HasCompactMulSupport.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [One β] [One γ] {f : αβ} {f' : αγ} (hf : ) (hff' : ) :
theorem HasCompactSupport.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [Zero β] [Zero γ] {g : βγ} {f : αβ} (hf : ) (hg : g 0 = 0) :
theorem HasCompactMulSupport.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [One β] [One γ] {g : βγ} {f : αβ} (hf : ) (hg : g 1 = 1) :
theorem hasCompactSupport_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [Zero β] [Zero γ] {g : βγ} {f : αβ} (hg : ∀ {x : β}, g x = 0 x = 0) :
theorem hasCompactMulSupport_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [] [One β] [One γ] {g : βγ} {f : αβ} (hg : ∀ {x : β}, g x = 1 x = 1) :
theorem HasCompactSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [Zero β] {f : αβ} (hf : ) {g : α'α} (hg : ) :
theorem HasCompactMulSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [One β] {f : αβ} (hf : ) {g : α'α} (hg : ) :
theorem HasCompactSupport.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [] [Zero β] [Zero γ] [Zero δ] {f : αβ} {f₂ : αγ} {m : βγδ} (hf : ) (hf₂ : ) (hm : m 0 0 = 0) :
HasCompactSupport fun (x : α) => m (f x) (f₂ x)
theorem HasCompactMulSupport.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [] [One β] [One γ] [One δ] {f : αβ} {f₂ : αγ} {m : βγδ} (hf : ) (hf₂ : ) (hm : m 1 1 = 1) :
HasCompactMulSupport fun (x : α) => m (f x) (f₂ x)
theorem HasCompactSupport.isCompact_preimage {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] (h'f : ) (hf : ) {k : Set β} (hk : ) (h'k : 0k) :
theorem HasCompactMulSupport.isCompact_preimage {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] (h'f : ) (hf : ) {k : Set β} (hk : ) (h'k : 1k) :
theorem HasCompactSupport.tsupport_extend_zero_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [Zero β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) :
theorem HasCompactMulSupport.mulTSupport_extend_one_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [One β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) :
theorem HasCompactSupport.extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [Zero β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) :
theorem HasCompactMulSupport.extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [One β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) :
theorem HasCompactSupport.tsupport_extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [Zero β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) (inj : ) :
tsupport () = g ''
theorem HasCompactMulSupport.mulTSupport_extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [] [] [One β] {f : αβ} [T2Space α'] (hf : ) {g : αα'} (cont : ) (inj : ) :
theorem HasCompactSupport.continuous_extend_zero {α' : Type u_3} {β : Type u_4} [] [Zero β] [T2Space α'] [] {U : Set α'} (hU : ) {f : Uβ} (cont : ) (supp : ) :
Continuous (Function.extend Subtype.val f 0)
theorem HasCompactMulSupport.continuous_extend_one {α' : Type u_3} {β : Type u_4} [] [One β] [T2Space α'] [] {U : Set α'} (hU : ) {f : Uβ} (cont : ) (supp : ) :
Continuous (Function.extend Subtype.val f 1)

## Functions with compact support: algebraic operations #

theorem HasCompactSupport.add {α : Type u_2} {β : Type u_4} [] [] {f : αβ} {f' : αβ} (hf : ) (hf' : ) :
theorem HasCompactMulSupport.mul {α : Type u_2} {β : Type u_4} [] [] {f : αβ} {f' : αβ} (hf : ) (hf' : ) :
theorem HasCompactSupport.smul_left {α : Type u_2} {M : Type u_7} {R : Type u_9} [] [] [] [] {f : αR} {f' : αM} (hf : ) :
theorem HasCompactSupport.smul_right {α : Type u_2} {M : Type u_7} {R : Type u_9} [] [Zero R] [Zero M] [] {f : αR} {f' : αM} (hf : ) :
theorem HasCompactSupport.smul_left' {α : Type u_2} {M : Type u_7} {R : Type u_9} [] [Zero R] [Zero M] [] {f : αR} {f' : αM} (hf : ) :
theorem HasCompactSupport.mul_right {α : Type u_2} {β : Type u_4} [] [] {f : αβ} {f' : αβ} (hf : ) :
theorem HasCompactSupport.mul_left {α : Type u_2} {β : Type u_4} [] [] {f : αβ} {f' : αβ} (hf : ) :
theorem LocallyFinite.exists_finset_nhd_support_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} [] {U : ιSet X} [Zero R] {f : ιXR} (hlf : LocallyFinite fun (i : ι) => Function.support (f i)) (hso : ∀ (i : ι), tsupport (f i) U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) :
∃ (is : ), nnhds x, n iis, U i zn, (Function.support fun (i : ι) => f i z) is

If a family of functions f has locally-finite support, subordinate to a family of open sets, then for any point we can find a neighbourhood on which only finitely-many members of f are non-zero.

theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} [] {U : ιSet X} [One R] {f : ιXR} (hlf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (hso : ∀ (i : ι), mulTSupport (f i) U i) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) :
∃ (is : ), nnhds x, n iis, U i zn, (Function.mulSupport fun (i : ι) => f i z) is

If a family of functions f has locally-finite multiplicative support, subordinate to a family of open sets, then for any point we can find a neighbourhood on which only finitely-many members of f are not equal to 1.

theorem locallyFinite_support_iff {X : Type u_1} {M : Type u_7} {ι : Type u_10} [] [] {f : ιXM} :
(LocallyFinite fun (i : ι) => Function.support (f i)) LocallyFinite fun (i : ι) => tsupport (f i)
theorem locallyFinite_mulSupport_iff {X : Type u_1} {M : Type u_7} {ι : Type u_10} [] [] {f : ιXM} :
(LocallyFinite fun (i : ι) => Function.mulSupport (f i)) LocallyFinite fun (i : ι) => mulTSupport (f i)
theorem LocallyFinite.smul_left {X : Type u_1} {M : Type u_7} {R : Type u_9} {ι : Type u_10} [] [Zero R] [Zero M] [] {s : ιXR} (h : LocallyFinite fun (i : ι) => Function.support (s i)) (f : ιXM) :
LocallyFinite fun (i : ι) => Function.support (s i f i)
theorem LocallyFinite.smul_right {X : Type u_1} {M : Type u_7} {R : Type u_9} {ι : Type u_10} [] [Zero M] [] {f : ιXM} (h : LocallyFinite fun (i : ι) => Function.support (f i)) (s : ιXR) :
LocallyFinite fun (i : ι) => Function.support (s i f i)