mathlib3 documentation

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 #

Implementation Notes #

def tsupport {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (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 α] [topological_space X] (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 α] [topological_space X] (f : X α) :
theorem subset_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (f : X α) :
theorem is_closed_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] [topological_space X] (f : X α) :
theorem is_closed_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (f : X α) :
theorem mul_tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [has_one α] [topological_space X] {f : X α} :
theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] {f : X α} :
theorem image_eq_one_of_nmem_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] [topological_space X] {f : X α} {x : X} (hx : x mul_tsupport f) :
f x = 1
theorem image_eq_zero_of_nmem_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] {f : X α} {x : X} (hx : x tsupport f) :
f x = 0
theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (f : X α) :
theorem tsupport_mul_subset_left {X : Type u_1} [topological_space X] {α : Type u_2} [mul_zero_class α] {f g : X α} :
tsupport (λ (x : X), f x * g x) tsupport f
theorem tsupport_mul_subset_right {X : Type u_1} [topological_space X] {α : Type u_2} [mul_zero_class α] {f g : X α} :
tsupport (λ (x : X), f x * g x) tsupport g
theorem tsupport_smul_subset_left {X : Type u_1} {M : Type u_2} {α : Type u_3} [topological_space X] [has_zero M] [has_zero α] [smul_with_zero M α] (f : X M) (g : X α) :
tsupport (λ (x : X), f x g x) tsupport f
theorem not_mem_tsupport_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {f : α β} {x : α} :
theorem not_mem_mul_tsupport_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α β} {x : α} :
theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] [topological_space β] {f : α β} (hf : (x : α), x tsupport f continuous_at f x) :
theorem continuous_of_mul_tsupport {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] [topological_space β] {f : α β} (hf : (x : α), x mul_tsupport f continuous_at f x) :
def has_compact_support {α : Type u_2} {β : Type u_4} [topological_space α] [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} [topological_space α] [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 exists_compact_iff_has_compact_support {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {f : α β} [t2_space α] :
( (K : set α), is_compact K (x : α), x K f x = 0) has_compact_support f
theorem exists_compact_iff_has_compact_mul_support {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α β} [t2_space α] :
( (K : set α), is_compact K (x : α), x K f x = 1) has_compact_mul_support f
theorem has_compact_support.intro {α : Type u_2} {β : Type u_4} [topological_space α] [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} [topological_space α] [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} [topological_space α] [has_zero β] {f : α β} (hf : has_compact_support f) :
theorem has_compact_support.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [topological_space α] [has_zero β] [has_zero γ] {f : α β} {f' : α γ} (hf : has_compact_support f) (hff' : function.support f' tsupport f) :
theorem has_compact_mul_support.mono' {α : Type u_2} {β : Type u_4} {γ : Type u_5} [topological_space α] [has_one β] [has_one γ] {f : α β} {f' : α γ} (hf : has_compact_mul_support f) (hff' : function.mul_support f' mul_tsupport f) :
theorem has_compact_mul_support.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [topological_space α] [has_one β] [has_one γ] {f : α β} {f' : α γ} (hf : has_compact_mul_support f) (hff' : function.mul_support f' function.mul_support f) :
theorem has_compact_support.mono {α : Type u_2} {β : Type u_4} {γ : Type u_5} [topological_space α] [has_zero β] [has_zero γ] {f : α β} {f' : α γ} (hf : has_compact_support f) (hff' : function.support f' function.support f) :
theorem has_compact_mul_support.comp_left {α : Type u_2} {β : Type u_4} {γ : Type u_5} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [topological_space α'] [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} [topological_space α] [topological_space α'] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [monoid_with_zero R] [add_monoid M] [distrib_mul_action R 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} [topological_space α] [has_zero R] [has_zero M] [smul_with_zero R 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} [topological_space α] [has_zero R] [has_zero M] [smul_with_zero R M] {f : α R} {f' : α M} (hf : has_compact_support f') :
theorem has_compact_support.mul_right {α : Type u_2} {β : Type u_4} [topological_space α] [mul_zero_class β] {f f' : α β} (hf : has_compact_support f) :
theorem has_compact_support.mul_left {α : Type u_2} {β : Type u_4} [topological_space α] [mul_zero_class β] {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} [topological_space 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} [topological_space 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.