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 #
- 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
functionnamespace, following many other topological definitions that are in the root namespace (compareEmbeddingvsFunction.Embedding).
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
- tsupport f = closure (Function.support f)
Instances For
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
isClosed_mulTSupport
{X : Type u_1}
{α : Type u_2}
[One α]
[TopologicalSpace X]
(f : X → α)
:
IsClosed (mulTSupport f)
theorem
mulTSupport_eq_empty_iff
{X : Type u_1}
{α : Type u_2}
[One α]
[TopologicalSpace X]
{f : X → α}
:
mulTSupport f = ∅ ↔ f = 1
theorem
image_eq_zero_of_nmem_tsupport
{X : Type u_1}
{α : Type u_2}
[Zero α]
[TopologicalSpace X]
{f : X → α}
{x : X}
(hx : ¬x ∈ tsupport f)
:
f x = 0
theorem
image_eq_one_of_nmem_mulTSupport
{X : Type u_1}
{α : Type u_2}
[One α]
[TopologicalSpace X]
{f : X → α}
{x : X}
(hx : ¬x ∈ mulTSupport f)
:
f x = 1
theorem
range_subset_insert_image_mulTSupport
{X : Type u_1}
{α : Type u_2}
[One α]
[TopologicalSpace X]
(f : X → α)
:
Set.range f ⊆ insert 1 (f '' mulTSupport f)
theorem
range_eq_image_mulTSupport_or
{X : Type u_1}
{α : Type u_2}
[One α]
[TopologicalSpace X]
(f : X → α)
:
Set.range f = f '' mulTSupport f ∨ Set.range f = insert 1 (f '' mulTSupport f)
theorem
tsupport_mul_subset_left
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_10}
[MulZeroClass α]
{f : X → α}
{g : X → α}
:
theorem
tsupport_mul_subset_right
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_10}
[MulZeroClass α]
{f : X → α}
{g : X → α}
:
theorem
tsupport_smul_subset_left
{X : Type u_1}
{M : Type u_10}
{α : Type u_11}
[TopologicalSpace X]
[Zero M]
[Zero α]
[SMulWithZero M α]
(f : X → M)
(g : X → α)
:
theorem
not_mem_mulTSupport_iff_eventuallyEq
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
{x : α}
:
theorem
continuous_of_tsupport
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
[TopologicalSpace β]
{f : α → β}
(hf : ∀ (x : α), x ∈ tsupport f → ContinuousAt f x)
:
theorem
continuous_of_mulTSupport
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
[TopologicalSpace β]
{f : α → β}
(hf : ∀ (x : α), x ∈ mulTSupport f → ContinuousAt f x)
:
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
- HasCompactSupport f = IsCompact (tsupport f)
Instances For
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}
[TopologicalSpace α]
[Zero β]
{f : α → β}
:
theorem
hasCompactMulSupport_def
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
:
theorem
exists_compact_iff_hasCompactSupport
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
{f : α → β}
[T2Space α]
:
theorem
exists_compact_iff_hasCompactMulSupport
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
[T2Space α]
:
theorem
HasCompactSupport.of_support_subset_isCompact
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
{f : α → β}
[T2Space α]
{K : Set α}
(hK : IsCompact K)
(h : Function.support f ⊆ K)
:
theorem
HasCompactMulSupport.of_mulSupport_subset_isCompact
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
[T2Space α]
{K : Set α}
(hK : IsCompact K)
(h : Function.mulSupport f ⊆ K)
:
theorem
HasCompactSupport.isCompact
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
{f : α → β}
(hf : HasCompactSupport f)
:
theorem
HasCompactMulSupport.isCompact
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
(hf : HasCompactMulSupport f)
:
IsCompact (mulTSupport f)
abbrev
hasCompactSupport_iff_eventuallyEq.match_1
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Zero β]
{f : α → β}
(motive : (∃ t, IsClosed t ∧ IsCompact t ∧ {x | (fun x => f x = OfNat.ofNat 0 x) x}ᶜ ⊆ t) → Prop)
:
Equations
- (_ : motive x) = (_ : motive x)
Instances For
theorem
hasCompactSupport_iff_eventuallyEq
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
{f : α → β}
:
theorem
hasCompactMulSupport_iff_eventuallyEq
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
:
theorem
HasCompactSupport.isCompact_range
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Zero β]
{f : α → β}
[TopologicalSpace β]
(h : HasCompactSupport f)
(hf : Continuous f)
:
theorem
HasCompactMulSupport.isCompact_range
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[One β]
{f : α → β}
[TopologicalSpace β]
(h : HasCompactMulSupport f)
(hf : Continuous f)
:
theorem
HasCompactSupport.mono'
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[Zero β]
[Zero γ]
{f : α → β}
{f' : α → γ}
(hf : HasCompactSupport f)
(hff' : Function.support f' ⊆ tsupport f)
:
theorem
HasCompactMulSupport.mono'
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[One β]
[One γ]
{f : α → β}
{f' : α → γ}
(hf : HasCompactMulSupport f)
(hff' : Function.mulSupport f' ⊆ mulTSupport f)
:
theorem
HasCompactSupport.mono
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[Zero β]
[Zero γ]
{f : α → β}
{f' : α → γ}
(hf : HasCompactSupport f)
(hff' : Function.support f' ⊆ Function.support f)
:
theorem
HasCompactMulSupport.mono
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[One β]
[One γ]
{f : α → β}
{f' : α → γ}
(hf : HasCompactMulSupport f)
(hff' : Function.mulSupport f' ⊆ Function.mulSupport f)
:
theorem
HasCompactSupport.comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[Zero β]
[Zero γ]
{g : β → γ}
{f : α → β}
(hf : HasCompactSupport f)
(hg : g 0 = 0)
:
HasCompactSupport (g ∘ f)
theorem
HasCompactMulSupport.comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[One β]
[One γ]
{g : β → γ}
{f : α → β}
(hf : HasCompactMulSupport f)
(hg : g 1 = 1)
:
HasCompactMulSupport (g ∘ f)
theorem
hasCompactSupport_comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[Zero β]
[Zero γ]
{g : β → γ}
{f : α → β}
(hg : ∀ {x : β}, g x = 0 ↔ x = 0)
:
HasCompactSupport (g ∘ f) ↔ HasCompactSupport f
theorem
hasCompactMulSupport_comp_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
[TopologicalSpace α]
[One β]
[One γ]
{g : β → γ}
{f : α → β}
(hg : ∀ {x : β}, g x = 1 ↔ x = 1)
:
HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
theorem
HasCompactSupport.comp_closedEmbedding
{α : Type u_2}
{α' : Type u_3}
{β : Type u_4}
[TopologicalSpace α]
[TopologicalSpace α']
[Zero β]
{f : α → β}
(hf : HasCompactSupport f)
{g : α' → α}
(hg : ClosedEmbedding g)
:
HasCompactSupport (f ∘ g)
theorem
HasCompactMulSupport.comp_closedEmbedding
{α : Type u_2}
{α' : Type u_3}
{β : Type u_4}
[TopologicalSpace α]
[TopologicalSpace α']
[One β]
{f : α → β}
(hf : HasCompactMulSupport f)
{g : α' → α}
(hg : ClosedEmbedding g)
:
HasCompactMulSupport (f ∘ g)
theorem
HasCompactSupport.comp₂_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[TopologicalSpace α]
[Zero β]
[Zero γ]
[Zero δ]
{f : α → β}
{f₂ : α → γ}
{m : β → γ → δ}
(hf : HasCompactSupport f)
(hf₂ : HasCompactSupport f₂)
(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}
[TopologicalSpace α]
[One β]
[One γ]
[One δ]
{f : α → β}
{f₂ : α → γ}
{m : β → γ → δ}
(hf : HasCompactMulSupport f)
(hf₂ : HasCompactMulSupport f₂)
(hm : m 1 1 = 1)
:
HasCompactMulSupport fun x => m (f x) (f₂ x)
theorem
HasCompactSupport.add
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[AddMonoid β]
{f : α → β}
{f' : α → β}
(hf : HasCompactSupport f)
(hf' : HasCompactSupport f')
:
HasCompactSupport (f + f')
theorem
HasCompactMulSupport.mul
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[Monoid β]
{f : α → β}
{f' : α → β}
(hf : HasCompactMulSupport f)
(hf' : HasCompactMulSupport f')
:
HasCompactMulSupport (f * f')
theorem
HasCompactSupport.smul_left
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[TopologicalSpace α]
[MonoidWithZero R]
[AddMonoid M]
[DistribMulAction R M]
{f : α → R}
{f' : α → M}
(hf : HasCompactSupport f')
:
HasCompactSupport (f • f')
theorem
HasCompactSupport.smul_right
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[TopologicalSpace α]
[Zero R]
[Zero M]
[SMulWithZero R M]
{f : α → R}
{f' : α → M}
(hf : HasCompactSupport f)
:
HasCompactSupport (f • f')
theorem
HasCompactSupport.smul_left'
{α : Type u_2}
{M : Type u_7}
{R : Type u_9}
[TopologicalSpace α]
[Zero R]
[Zero M]
[SMulWithZero R M]
{f : α → R}
{f' : α → M}
(hf : HasCompactSupport f')
:
HasCompactSupport (f • f')
theorem
HasCompactSupport.mul_right
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[MulZeroClass β]
{f : α → β}
{f' : α → β}
(hf : HasCompactSupport f)
:
HasCompactSupport (f * f')
theorem
HasCompactSupport.mul_left
{α : Type u_2}
{β : Type u_4}
[TopologicalSpace α]
[MulZeroClass β]
{f : α → β}
{f' : α → β}
(hf : HasCompactSupport f')
:
HasCompactSupport (f * f')
theorem
LocallyFinite.exists_finset_nhd_support_subset
{X : Type u_1}
{R : Type u_9}
{ι : Type u_10}
{U : ι → Set X}
[TopologicalSpace X]
[Zero R]
{f : ι → X → R}
(hlf : LocallyFinite fun i => Function.support (f i))
(hso : ∀ (i : ι), tsupport (f i) ⊆ U i)
(ho : ∀ (i : ι), IsOpen (U i))
(x : X)
:
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}
[TopologicalSpace X]
[One R]
{f : ι → X → R}
(hlf : LocallyFinite fun i => Function.mulSupport (f i))
(hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i)
(ho : ∀ (i : ι), IsOpen (U i))
(x : X)
:
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.