# Documentation

Mathlib.Topology.Support

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

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.

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 => f x * g x)
theorem tsupport_mul_subset_right {X : Type u_1} [] {α : Type u_10} [] {f : Xα} {g : Xα} :
(tsupport fun 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 => f x g x)
theorem not_mem_tsupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} {x : α} :
theorem not_mem_mulTSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} {x : α} :
theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [] [Zero β] [] {f : αβ} (hf : ∀ (x : α), x ) :
theorem continuous_of_mulTSupport {α : Type u_2} {β : Type u_4} [] [One β] [] {f : αβ} (hf : ∀ (x : α), x ) :
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.

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.

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, ∀ (x : α), ¬x Kf x = 0)
theorem exists_compact_iff_hasCompactMulSupport {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] :
(K, ∀ (x : α), ¬x Kf x = 1)
theorem HasCompactSupport.intro {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} [] {K : Set α} (hK : ) (hfK : ∀ (x : α), ¬x Kf x = 0) :
theorem HasCompactMulSupport.intro {α : Type u_2} {β : Type u_4} [] [One β] {f : αβ} [] {K : Set α} (hK : ) (hfK : ∀ (x : α), ¬x Kf 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 : ) :
abbrev hasCompactSupport_iff_eventuallyEq.match_1 {α : Type u_1} {β : Type u_2} [] [Zero β] {f : αβ} (motive : (t, {x | (fun x => f x = OfNat.ofNat (αβ) 0 Zero.toOfNat0 x) x} t) → Prop) :
(x : t, {x | (fun x => f x = OfNat.ofNat (αβ) 0 Zero.toOfNat0 x) x} t) → ((_C : Set α) → (hC : IsClosed _C {x | (fun x => f x = OfNat.ofNat (αβ) 0 Zero.toOfNat0 x) x} _C) → motive (_ : t, {x | (fun x => f x = OfNat.ofNat (αβ) 0 Zero.toOfNat0 x) x} t)) → motive x
Instances For
theorem hasCompactSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [Zero β] {f : αβ} :
theorem hasCompactMulSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [] [One β] {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.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 n, n nhds x n ⋂ (i : ι) (_ : i is), U i ∀ (z : X), z n(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 n, n nhds x n ⋂ (i : ι) (_ : i is), U i ∀ (z : X), z n(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.