mathlib documentation

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 #

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_zero_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_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (f : X → α) :
theorem range_subset_insert_image_mul_tsupport {X : Type u_1} {α : Type u_2} [has_one α] [topological_space X] (f : X → α) :
theorem range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [has_zero α] [topological_space X] (f : X → α) :
theorem range_eq_image_mul_tsupport_or {X : Type u_1} {α : Type u_2} [has_one α] [topological_space X] (f : X → α) :
theorem not_mem_closure_mul_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α → β} {x : α} :
theorem not_mem_closure_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {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 has_compact_support_def {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {f : α → β} :
theorem has_compact_mul_support_def {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α → β} :
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 Kf 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 Kf 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 Kf 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 Kf 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_mul_support.is_compact {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α → β} (hf : has_compact_mul_support f) :
theorem has_compact_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {f : α → β} :
theorem has_compact_mul_support_iff_eventually_eq {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α → β} :
theorem has_compact_mul_support.is_compact_range {α : Type u_2} {β : Type u_4} [topological_space α] [has_one β] {f : α → β} [topological_space β] (h : has_compact_mul_support f) (hf : continuous f) :
theorem has_compact_support.is_compact_range {α : Type u_2} {β : Type u_4} [topological_space α] [has_zero β] {f : α → β} [topological_space β] (h : has_compact_support f) (hf : continuous 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 nfunction.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 nfunction.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.