topology.support

# The topological support of a function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• function.mul_tsupport & function.tsupport
• function.has_compact_mul_support & function.has_compact_support

## 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} [has_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
def mul_tsupport {X : Type u_1} {α : Type u_2} [has_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
theorem subset_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] (f : X α) :
theorem subset_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] (f : X α) :
theorem is_closed_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] (f : X α) :
theorem is_closed_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] (f : X α) :
theorem mul_tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [has_one α] {f : X α} :
f = 1
theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [has_zero α] {f : X α} :
f = 0
theorem image_eq_one_of_nmem_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] {f : X α} {x : X} (hx : x ) :
f x = 1
theorem image_eq_zero_of_nmem_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] {f : X α} {x : X} (hx : x ) :
f x = 0
theorem range_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] (f : X α) :
(f '' tsupport f)
theorem range_subset_insert_image_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] (f : X α) :
(f ''
theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [has_zero α] (f : X α) :
= f '' = (f '' tsupport f)
theorem range_eq_image_mul_tsupport_or {X : Type u_1} {α : Type u_2} [has_one α] (f : X α) :
= = (f ''
theorem tsupport_mul_subset_left {X : Type u_1} {α : Type u_2} {f g : X α} :
tsupport (λ (x : X), f x * g x)
theorem tsupport_mul_subset_right {X : Type u_1} {α : Type u_2} {f g : X α} :
tsupport (λ (x : X), f x * g x)
theorem tsupport_smul_subset_left {X : Type u_1} {M : Type u_2} {α : Type u_3} [has_zero M] [has_zero α] [ α] (f : X M) (g : X α) :
tsupport (λ (x : X), f x g x)
theorem not_mem_tsupport_iff_eventually_eq {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} {x : α} :
theorem not_mem_mul_tsupport_iff_eventually_eq {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} {x : α} :
theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} (hf : (x : α), x ) :
theorem continuous_of_mul_tsupport {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} (hf : (x : α), ) :
def has_compact_support {α : Type u_2} {β : Type u_4} [has_zero β] (f : α β) :
Prop

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
def has_compact_mul_support {α : Type u_2} {β : Type u_4} [has_one β] (f : α β) :
Prop

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
theorem has_compact_support_def {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} :
theorem has_compact_mul_support_def {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} :
theorem exists_compact_iff_has_compact_support {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} [t2_space α] :
( (K : set α), (x : α), x K f x = 0)
theorem exists_compact_iff_has_compact_mul_support {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} [t2_space α] :
( (K : set α), (x : α), x K f x = 1)
theorem has_compact_support.intro {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} [t2_space α] {K : set α} (hK : is_compact K) (hfK : (x : α), x K f x = 0) :
theorem has_compact_mul_support.intro {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} [t2_space α] {K : set α} (hK : is_compact K) (hfK : (x : α), x K f x = 1) :
theorem has_compact_support.is_compact {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} (hf : has_compact_support f) :
theorem has_compact_mul_support.is_compact {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} (hf : has_compact_mul_support f) :
theorem has_compact_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} :
theorem has_compact_mul_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} :
theorem has_compact_mul_support.is_compact_range {α : Type u_2} {β : Type u_4} [has_one β] {f : α β} (h : has_compact_mul_support f) (hf : continuous f) :
theorem has_compact_support.is_compact_range {α : Type u_2} {β : Type u_4} [has_zero β] {f : α β} (h : has_compact_support f) (hf : continuous f) :
theorem has_compact_support.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_zero β] [has_zero γ] {f : α β} {f' : α γ} (hf : has_compact_support f) (hff' : ) :
theorem has_compact_mul_support.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_one β] [has_one γ] {f : α β} {f' : α γ} (hf : has_compact_mul_support f) (hff' : ) :
theorem has_compact_mul_support.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_one β] [has_one γ] {f : α β} {f' : α γ} (hf : has_compact_mul_support f) (hff' : ) :
theorem has_compact_support.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_zero β] [has_zero γ] {f : α β} {f' : α γ} (hf : has_compact_support f) (hff' : ) :
theorem has_compact_mul_support.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_one β] [has_one γ] {g : β γ} {f : α β} (hf : has_compact_mul_support f) (hg : g 1 = 1) :
theorem has_compact_support.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_zero β] [has_zero γ] {g : β γ} {f : α β} (hf : has_compact_support f) (hg : g 0 = 0) :
theorem has_compact_support_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_zero β] [has_zero γ] {g : β γ} {f : α β} (hg : {x : β}, g x = 0 x = 0) :
theorem has_compact_mul_support_comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [has_one β] [has_one γ] {g : β γ} {f : α β} (hg : {x : β}, g x = 1 x = 1) :
theorem has_compact_support.comp_closed_embedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [has_zero β] {f : α β} (hf : has_compact_support f) {g : α' α} (hg : closed_embedding g) :
theorem has_compact_mul_support.comp_closed_embedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [has_one β] {f : α β} (hf : has_compact_mul_support f) {g : α' α} (hg : closed_embedding g) :
theorem has_compact_support.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_zero β] [has_zero γ] [has_zero δ] {f : α β} {f₂ : α γ} {m : β γ δ} (hf : has_compact_support f) (hf₂ : has_compact_support f₂) (hm : m 0 0 = 0) :
has_compact_support (λ (x : α), m (f x) (f₂ x))
theorem has_compact_mul_support.comp₂_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_one β] [has_one γ] [has_one δ] {f : α β} {f₂ : α γ} {m : β γ δ} (hf : has_compact_mul_support f) (hf₂ : has_compact_mul_support f₂) (hm : m 1 1 = 1) :
has_compact_mul_support (λ (x : α), m (f x) (f₂ x))
theorem has_compact_support.add {α : Type u_2} {β : Type u_4} [add_monoid β] {f f' : α β} (hf : has_compact_support f) (hf' : has_compact_support f') :
theorem has_compact_mul_support.mul {α : Type u_2} {β : Type u_4} [monoid β] {f f' : α β} (hf : has_compact_mul_support f) (hf' : has_compact_mul_support f') :
theorem has_compact_support.smul_left {α : Type u_2} {M : Type u_7} {R : Type u_9} [add_monoid M] [ M] {f : α R} {f' : α M} (hf : has_compact_support f') :
theorem has_compact_support.smul_right {α : Type u_2} {M : Type u_7} {R : Type u_9} [has_zero R] [has_zero M] [ M] {f : α R} {f' : α M} (hf : has_compact_support f) :
theorem has_compact_support.smul_left' {α : Type u_2} {M : Type u_7} {R : Type u_9} [has_zero R] [has_zero M] [ M] {f : α R} {f' : α M} (hf : has_compact_support f') :
theorem has_compact_support.mul_right {α : Type u_2} {β : Type u_4} {f f' : α β} (hf : has_compact_support f) :
theorem has_compact_support.mul_left {α : Type u_2} {β : Type u_4} {f f' : α β} (hf : has_compact_support f') :
theorem locally_finite.exists_finset_nhd_mul_support_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} {U : ι set X} [has_one R] {f : ι X R} (hlf : locally_finite (λ (i : ι), function.mul_support (f i))) (hso : (i : ι), mul_tsupport (f i) U i) (ho : (i : ι), is_open (U i)) (x : X) :
(is : finset ι) {n : set X} (hn₁ : n nhds x) (hn₂ : n (i : ι) (H : i is), U i), (z : X), z n function.mul_support (λ (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 locally_finite.exists_finset_nhd_support_subset {X : Type u_1} {R : Type u_9} {ι : Type u_10} {U : ι set X} [has_zero R] {f : ι X R} (hlf : locally_finite (λ (i : ι), function.support (f i))) (hso : (i : ι), tsupport (f i) U i) (ho : (i : ι), is_open (U i)) (x : X) :
(is : finset ι) {n : set X} (hn₁ : n nhds x) (hn₂ : n (i : ι) (H : i is), U i), (z : X), z n function.support (λ (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.