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

TODO

The definitions have been put in the root namespace following many other topological definitions, like Embedding. Since then, Embedding was renamed to Topology.IsEmbedding, so it might be worth reconsidering namespacing the definitions here.

def mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace 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

• mulTSupport f = closure (Function.mulSupport f)

def tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace 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

• tsupport f = closure (Function.support f)

theorem subset_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : Function.mulSupport f ⊆ mulTSupport f

theorem subset_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Function.support f ⊆ tsupport f

theorem isClosed_mulTSupport {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] (f : X → α) : IsClosed (mulTSupport f)

theorem isClosed_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : IsClosed (tsupport f)

theorem mulTSupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [One α] [TopologicalSpace X] {f : X → α} : mulTSupport f = ∅ ↔ f = 1

theorem tsupport_eq_empty_iff {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] {f : X → α} : tsupport f = ∅ ↔ f = 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 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 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_subset_insert_image_tsupport {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Set.range f ⊆ insert 0 (f '' tsupport 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 range_eq_image_tsupport_or {X : Type u_1} {α : Type u_2} [Zero α] [TopologicalSpace X] (f : X → α) : Set.range f = f '' tsupport f ∨ Set.range f = insert 0 (f '' tsupport f)

theorem tsupport_mul_subset_left {X : Type u_1} [TopologicalSpace X] {α : Type u_9} [MulZeroClass α] {f g : X → α} : (tsupport fun (x : X) => f x * g x) ⊆ tsupport f

theorem tsupport_mul_subset_right {X : Type u_1} [TopologicalSpace X] {α : Type u_9} [MulZeroClass α] {f g : X → α} : (tsupport fun (x : X) => f x * g x) ⊆ tsupport g

theorem tsupport_smul_subset_left {X : Type u_1} {M : Type u_9} {α : Type u_10} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α] (f : X → M) (g : X → α) : (tsupport fun (x : X) => f x • g x) ⊆ tsupport f

theorem tsupport_smul_subset_right {X : Type u_1} {M : Type u_9} {α : Type u_10} [TopologicalSpace X] [Zero α] [SMulZeroClass M α] (f : X → M) (g : X → α) : (tsupport fun (x : X) => f x • g x) ⊆ tsupport g

theorem mulTSupport_mul {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [Monoid α] {f g : X → α} : (mulTSupport fun (x : X) => f x * g x) ⊆ mulTSupport f ∪ mulTSupport g

theorem tsupport_add {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [AddMonoid α] {f g : X → α} : (tsupport fun (x : X) => f x + g x) ⊆ tsupport f ∪ tsupport g

theorem not_mem_mulTSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {x : α} : x ∉ mulTSupport f ↔ f =ᶠ[nhds x] 1

theorem not_mem_tsupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {x : α} : x ∉ tsupport f ↔ f =ᶠ[nhds x] 0

theorem continuous_of_mulTSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] [TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ mulTSupport f, ContinuousAt f x) : Continuous f

theorem continuous_of_tsupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] [TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ tsupport f, ContinuousAt f x) : Continuous f

Functions with compact support

def HasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [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

• HasCompactMulSupport f = IsCompact (mulTSupport f)

def HasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [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

• HasCompactSupport f = IsCompact (tsupport f)

theorem hasCompactMulSupport_def {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} : HasCompactMulSupport f ↔ IsCompact (closure (Function.mulSupport f))

theorem hasCompactSupport_def {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ IsCompact (closure (Function.support f))

theorem exists_compact_iff_hasCompactMulSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

theorem exists_compact_iff_hasCompactSupport {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f

theorem HasCompactMulSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 1) : HasCompactMulSupport f

theorem HasCompactSupport.intro {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f

theorem HasCompactMulSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x ∉ K, f x = 1) : HasCompactMulSupport f

theorem HasCompactSupport.intro' {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f

theorem HasCompactMulSupport.of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (h : Function.mulSupport f ⊆ K) : HasCompactMulSupport f

theorem HasCompactSupport.of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] {K : Set α} (hK : IsCompact K) (h : Function.support f ⊆ K) : HasCompactSupport f

theorem HasCompactMulSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f)

theorem HasCompactSupport.isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} (hf : HasCompactSupport f) : IsCompact (tsupport f)

theorem hasCompactMulSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} : HasCompactMulSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 1

theorem hasCompactSupport_iff_eventuallyEq {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 0

theorem isCompact_range_of_mulSupport_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.mulSupport f ⊆ k) : IsCompact (Set.range f)

theorem isCompact_range_of_support_subset_isCompact {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.support f ⊆ k) : IsCompact (Set.range f)

theorem HasCompactMulSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous f) : IsCompact (Set.range f)

theorem HasCompactSupport.isCompact_range {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (h : HasCompactSupport f) (hf : Continuous f) : IsCompact (Set.range 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) : HasCompactMulSupport 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) : HasCompactSupport 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) : HasCompactMulSupport 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) : HasCompactSupport 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 : α → β} (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 : α → β} (hg : ∀ {x : β}, g x = 1 ↔ x = 1) : HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport 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_isClosedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} (hf : HasCompactMulSupport f) {g : α' → α} (hg : Topology.IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g)

theorem HasCompactSupport.comp_isClosedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} (hf : HasCompactSupport f) {g : α' → α} (hg : Topology.IsClosedEmbedding g) : HasCompactSupport (f ∘ g)

@[deprecated HasCompactMulSupport.comp_isClosedEmbedding (since := "2024-10-20")]

theorem HasCompactMulSupport.comp_closedEmbedding {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} (hf : HasCompactMulSupport f) {g : α' → α} (hg : Topology.IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g)

Alias of HasCompactMulSupport.comp_isClosedEmbedding.

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.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.isCompact_preimage {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [One β] {f : α → β} [TopologicalSpace β] (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k) (h'k : 1 ∉ k) : IsCompact (f ⁻¹' k)

theorem HasCompactSupport.isCompact_preimage {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (h'f : HasCompactSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k) (h'k : 0 ∉ k) : IsCompact (f ⁻¹' k)

theorem HasCompactMulSupport.mulTSupport_extend_one_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) : mulTSupport (Function.extend g f 1) ⊆ g '' mulTSupport f

theorem HasCompactSupport.tsupport_extend_zero_subset {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : tsupport (Function.extend g f 0) ⊆ g '' tsupport f

theorem HasCompactMulSupport.extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) : HasCompactMulSupport (Function.extend g f 1)

theorem HasCompactSupport.extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : HasCompactSupport (Function.extend g f 0)

theorem HasCompactMulSupport.mulTSupport_extend_one {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [One β] {f : α → β} [T2Space α'] (hf : HasCompactMulSupport f) {g : α → α'} (cont : Continuous g) (inj : Function.Injective g) : mulTSupport (Function.extend g f 1) = g '' mulTSupport f

theorem HasCompactSupport.tsupport_extend_zero {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) (inj : Function.Injective g) : tsupport (Function.extend g f 0) = g '' tsupport f

theorem HasCompactMulSupport.continuous_extend_one {α' : Type u_3} {β : Type u_4} [TopologicalSpace α'] [One β] [T2Space α'] [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : ↑U → β} (cont : Continuous f) (supp : HasCompactMulSupport f) : Continuous (Function.extend Subtype.val f 1)

theorem HasCompactSupport.continuous_extend_zero {α' : Type u_3} {β : Type u_4} [TopologicalSpace α'] [Zero β] [T2Space α'] [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : ↑U → β} (cont : Continuous f) (supp : HasCompactSupport f) : Continuous (Function.extend Subtype.val f 0)

theorem HasCompactMulSupport.is_one_at_infty {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [One γ] {f : α → γ} [TopologicalSpace γ] (h : HasCompactMulSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 1)

If f has compact multiplicative support, then f tends to 1 at infinity.

theorem HasCompactSupport.is_zero_at_infty {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] {f : α → γ} [TopologicalSpace γ] (h : HasCompactSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 0)

If f has compact support, then f tends to zero at infinity.

theorem HasCompactMulSupport.of_compactSpace {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [One γ] [CompactSpace α] (f : α → γ) : HasCompactMulSupport f

In a compact space α, any function has compact support.

theorem HasCompactSupport.of_compactSpace {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] [CompactSpace α] (f : α → γ) : HasCompactSupport f

Functions with compact support: algebraic operations

theorem HasCompactMulSupport.mul {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulOneClass β] {f f' : α → β} (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') : HasCompactMulSupport (f * f')

theorem HasCompactSupport.add {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddZeroClass β] {f f' : α → β} (hf : HasCompactSupport f) (hf' : HasCompactSupport f') : HasCompactSupport (f + f')

@[simp]

theorem HasCompactMulSupport.one {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [One β] : HasCompactMulSupport 1

theorem HasCompactSupport.zero {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [Zero β] : HasCompactSupport 0

theorem HasCompactMulSupport.inv' {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [DivisionMonoid β] {f : α → β} (hf : HasCompactMulSupport f) : HasCompactMulSupport f⁻¹

theorem HasCompactSupport.neg' {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [SubtractionMonoid β] {f : α → β} (hf : HasCompactSupport f) : HasCompactSupport (-f)

theorem HasCompactSupport.smul_left {α : Type u_2} {M : Type u_7} {R : Type u_8} [TopologicalSpace α] [Zero M] [SMulZeroClass 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_8} [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 HasCompactSupport.abs {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddGroup β] [Lattice β] [AddLeftMono β] {f : α → β} (hf : HasCompactSupport f) : HasCompactSupport |f|

theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {X : Type u_1} {R : Type u_8} {ι : Type u_9} [TopologicalSpace X] {U : ι → Set 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) : ∃ (is : Finset ι), ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ 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.

theorem LocallyFinite.exists_finset_nhd_support_subset {X : Type u_1} {R : Type u_8} {ι : Type u_9} [TopologicalSpace X] {U : ι → Set 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) : ∃ (is : Finset ι), ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ 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_mulSupport_iff {X : Type u_1} {M : Type u_7} {ι : Type u_9} [TopologicalSpace X] [CommMonoid M] {f : ι → X → M} : (LocallyFinite fun (i : ι) => Function.mulSupport (f i)) ↔ LocallyFinite fun (i : ι) => mulTSupport (f i)

theorem locallyFinite_support_iff {X : Type u_1} {M : Type u_7} {ι : Type u_9} [TopologicalSpace X] [AddCommMonoid M] {f : ι → X → M} : (LocallyFinite fun (i : ι) => Function.support (f i)) ↔ LocallyFinite fun (i : ι) => tsupport (f i)

theorem LocallyFinite.smul_left {X : Type u_1} {M : Type u_7} {R : Type u_8} {ι : Type u_9} [TopologicalSpace X] [Zero R] [Zero M] [SMulWithZero R M] {s : ι → X → R} (h : LocallyFinite fun (i : ι) => Function.support (s i)) (f : ι → X → M) : LocallyFinite fun (i : ι) => Function.support (s i • f i)

theorem LocallyFinite.smul_right {X : Type u_1} {M : Type u_7} {R : Type u_8} {ι : Type u_9} [TopologicalSpace X] [Zero M] [SMulZeroClass R M] {f : ι → X → M} (h : LocallyFinite fun (i : ι) => Function.support (f i)) (s : ι → X → R) : LocallyFinite fun (i : ι) => Function.support (s i • f i)