isClosed_tsupport
theorem isClosed_tsupport :
∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α), IsClosed (tsupport f)
The theorem `isClosed_tsupport` states that for any type `X` endowed with a topological space structure, and for any type `α` that has a zero element, the topological support (i.e., the closure of the set of all points where the function is nonzero) of any function `f` from `X` to `α` is a closed set in `X`. In other words, if you have a function that maps points in a topological space to values which include a concept of 'zero', the set of points where the function isn't 'zero' and all of its limit points make up a closed set.
More concisely: For any function $f$ from a topological space $X$ to a type with a zero element, the topological support of $f$ is a closed set in $X$.
|
subset_tsupport
theorem subset_tsupport :
∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
Function.support f ⊆ tsupport f
This theorem states that for any function `f` from a type `X` to a type `α`, where `α` has a zero element and `X` has a topological space structure, the support of `f` (i.e. the set of all points `x` in `X` where `f(x)` is not zero) is always a subset of the topological support of `f` (i.e. the closure of the support of `f` in the topology of `X`). In other words, all points where the function `f` is nonzero are contained within the closure of those points in the underlying topological space.
More concisely: The support of a function from a topological space to a type with a zero element is contained in the topological closure of its support.
|
HasCompactMulSupport.isCompact_range
theorem HasCompactMulSupport.isCompact_range :
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β}
[inst_2 : TopologicalSpace β], HasCompactMulSupport f → Continuous f → IsCompact (Set.range f)
This theorem states that for any types `α` and `β`, where `α` has a topological space structure and `β` is equipped with both a topological space structure and an operation `One`, if a function `f` from `α` to `β` has compact multiplicative support and is a continuous function, then the range of `f` is a compact set. In mathematical terms, if the closure of the multiplicative support of `f` is compact and `f` is a continuous function, then the set of all possible outputs of `f` is also compact.
More concisely: If `f` is a continuous function from a compact, topologically closed subset of a topological space `α` to a topological space `β` with operation `One`, then the range of `f` is a compact set.
|
HasCompactMulSupport.mulTSupport_extend_one_subset
theorem HasCompactMulSupport.mulTSupport_extend_one_subset :
∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
[inst_2 : One β] {f : α → β} [inst_3 : T2Space α'],
HasCompactMulSupport f →
∀ {g : α → α'}, Continuous g → mulTSupport (Function.extend g f 1) ⊆ g '' mulTSupport f
This theorem states that for any types `α`, `α'`, and `β`, if `α` and `α'` are topological spaces, `β` has a one element, and `α'` is a T2 space (also known as a Hausdorff space), then for any function `f` from `α` to `β` that has compact multiplicative support, and any continuous function `g` from `α` to `α'`, the topological multiplicative support of the function that extends `g` and `f` by `1` is a subset of the image of the function `g` applied to the topological multiplicative support of the function `f`. Here, the topological multiplicative support of a function is the closure of the set of all elements where the function is not equal to `1`, and a function having compact multiplicative support means that the closure of its multiplicative support is compact.
More concisely: If `f: α → β` is a continuous function from a compactly supported, compact topological space `α` to a Hausdorff space `β` with a one-point topology, and `g: α → α'` is a continuous function, then the topological support of `f ⊤ g` (the extension of `g` and `f` by 1) is contained in the image of `g` applied to the topological support of `f`.
|
LocallyFinite.exists_finset_nhd_mulSupport_subset
theorem LocallyFinite.exists_finset_nhd_mulSupport_subset :
∀ {X : Type u_1} {R : Type u_9} {ι : Type u_10} [inst : TopologicalSpace X] {U : ι → Set X} [inst_1 : One R]
{f : ι → X → R},
(LocallyFinite fun i => Function.mulSupport (f i)) →
(∀ (i : ι), mulTSupport (f i) ⊆ U i) →
(∀ (i : ι), IsOpen (U i)) →
∀ (x : X), ∃ is, ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.mulSupport fun i => f i z) ⊆ ↑is
This theorem states that if we have a family of functions `f`, where each function's multiplicative support (the set of points where the function is not equal to 1) is locally finite (meaning, around each point, there is a neighborhood that intersects with only finitely many of these multiplicative supports), and each function's topological support (the closure of its multiplicative support) is contained within a corresponding open set `U`, then for any given point, we can find a neighborhood such that only finitely many members of the family of functions are unequal to 1 in this neighborhood. This neighborhood is also contained within the intersection of the open sets `U` corresponding to these functions.
More concisely: If `{f_i}`, a family of functions with locally finite and contained multiplicative supports, admits a common refinement of their open containment `U_i`, then for any point, there exists a neighborhood contained in the intersection of the `U_i` where only finitely many `f_i` are not equal to 1.
|
image_eq_zero_of_nmem_tsupport
theorem image_eq_zero_of_nmem_tsupport :
∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] {f : X → α} {x : X},
x ∉ tsupport f → f x = 0
This theorem states that for any given function `f` from a type `X` to a type `α`, where `α` has a zero element and `X` has a topological structure, if an element `x` of `X` does not belong to the topological support of the function `f` (i.e., it is not in the closure of the set of all elements where the function is nonzero), then the value of the function `f` at `x` is zero. In other words, in terms of function support, if `x` is outside the topological support of `f`, then `f(x)` is zero.
More concisely: If a function `f` from a topological space `X` to a type `α` with a zero element, has no nonzero values in the closure of a point `x` in `X`, then `f(x) = 0`.
|
hasCompactSupport_def
theorem hasCompactSupport_def :
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β},
HasCompactSupport f ↔ IsCompact (closure (Function.support f))
This theorem states that for any function `f` from a type `α` to a type `β`, where `α` has a topological space structure and `β` has a zero element, the function `f` has compact support if and only if the closure of the support of the function `f` is compact. In other words, a function `f` is said to have compact support when the smallest closed set that contains all the points `x` for which `f(x)` is not zero, is a compact set. Here, a set is compact if for every nontrivial filter that contains the set, there exists a point in the set such that every set in the filter intersects with every neighborhood of this point.
More concisely: A function from a compact space to a space with a zero element has compact support if and only if its support's closure is a compact set.
|
HasCompactSupport.mono'
theorem HasCompactSupport.mono' :
∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
{f : α → β} {f' : α → γ}, HasCompactSupport f → Function.support f' ⊆ tsupport f → HasCompactSupport f'
The theorem `HasCompactSupport.mono'` states that for any types `α`, `β`, and `γ` where `α` is a topological space and `β` and `γ` are equipped with a zero element, if a function `f` from `α` to `β` has compact support and the support of another function `f'` from `α` to `γ` is a subset of the topological support of `f`, then `f'` also has compact support. In simpler terms, if a function is zero outside a compact set and another function is also zero where the first function is zero, then the second function also has compact support.
More concisely: If a function from a topological space to a Hausdorff space with a zero element has compact support, and another function from the same space to the same space with a zero element has support contained in the topological support of the first function, then the second function also has compact support.
|
hasCompactSupport_iff_eventuallyEq
theorem hasCompactSupport_iff_eventuallyEq :
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β},
HasCompactSupport f ↔ (Filter.coclosedCompact α).EventuallyEq f 0
The theorem states that for any function `f` from a type `α` to `β`, where `α` is a topological space and `β` is a type with zero, `f` has compact support if and only if `f` is eventually equal to zero with respect to the filter generated by complements to closed compact sets in `α`. In other words, the support of `f` is compact if and only if `f` is zero outside a compact subset of `α`, considering the topology that `α` is endowed with.
More concisely: A function `f` from a topological space `α` to a type `β` with zero has compact support if and only if it is equal to zero in the filter generated by complements of closed compact sets in `α`.
|
not_mem_tsupport_iff_eventuallyEq
theorem not_mem_tsupport_iff_eventuallyEq :
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {x : α},
x ∉ tsupport f ↔ (nhds x).EventuallyEq f 0
This theorem states that for any type `α` with a topology, type `β` with zero, a function `f` from `α` to `β`, and an element `x` of `α`, `x` is not in the topological support of `f` if and only if the function `f` is eventually equal to zero around `x`. In other words, `x` does not belong to the closure of the set where `f` is nonzero if and only if for all neighborhoods of `x` (as defined by the neighborhood filter `nhds x`), `f` equals zero almost everywhere in those neighborhoods.
More concisely: For any continuous function $f : X \to Y$ where $X$ is a topological space, $Y$ has a zero element, and $x \in X$, $x$ is not in the closure of $f^{-1}(Y \setminus \{0\})$ if and only if $f(x) = 0$ and $f$ is zero in a neighborhood of $x$.
|
HasCompactSupport.tsupport_extend_zero_subset
theorem HasCompactSupport.tsupport_extend_zero_subset :
∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
[inst_2 : Zero β] {f : α → β} [inst_3 : T2Space α'],
HasCompactSupport f → ∀ {g : α → α'}, Continuous g → tsupport (Function.extend g f 0) ⊆ g '' tsupport f
This theorem states that for any two types `α` and `α'` and any type `β` with a zero element, if we have a function `f` from `α` to `β` that has compact support and another function `g` from `α` to `α'` that is continuous, then the topological support of the function resulting from extending `f` by `g` (i.e., replacing values of `f` outside its domain with zeros) is a subset of the image under `g` of the topological support of `f`. This theorem assumes that the topological spaces `α` and `α'` satisfy the T2 separation axiom, also known as the Hausdorff condition.
More concisely: Given functions `f` from type `α` to `β` with compact support, `g` from `α` to `α'`, and assuming `α`, `α'` are T2 spaces, the topological support of the extended function `f ↦ 0 on α \ dom(f) ∪ {g(x) : x ∈ α}` is a subset of `g''(supp(f))`, where `g''` is the continuous function from `α'` to `β` extending `f` by zero.
|
subset_mulTSupport
theorem subset_mulTSupport :
∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α),
Function.mulSupport f ⊆ mulTSupport f
The theorem `subset_mulTSupport` states that for any type `X` with a topology and any type `α` with a multiplicative identity (denoted `One α`), for any function `f` from `X` to `α`, the multiplicative support of `f` (i.e., the set of points `x` in `X` such that `f(x)` is not equal to the multiplicative identity of `α`) is a subset of the topological multiplicative support of `f` (i.e., the closure of the set of all points where the function is not equal to the multiplicative identity). In other words, every point where the function doesn't yield the multiplicative identity is contained in the set of limit points of the set where the function doesn't yield the multiplicative identity.
More concisely: The multiplicative support of a function from a topological space to a type with a multiplicative identity is contained in the topological closure of its non-identity values.
|
HasCompactSupport.isCompact_range
theorem HasCompactSupport.isCompact_range :
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β}
[inst_2 : TopologicalSpace β], HasCompactSupport f → Continuous f → IsCompact (Set.range f)
This theorem states that if a function 'f' from a topological space 'α' to another topological space 'β' has compact support and is continuous, then the range of 'f' is a compact set. In other words, for every nontrivial filter that contains the range of 'f', there is a point in the range such that every set of the filter intersects every neighborhood of this point. This encapsulates a fundamental property of continuous functions with compact support in the context of topological spaces.
More concisely: If $f:\alpha \to \beta$ is a continuous function with compact support from a topological space $\alpha$ to another topological space $\beta$, then the range of $f$ is a compact set.
|
LocallyFinite.exists_finset_nhd_support_subset
theorem LocallyFinite.exists_finset_nhd_support_subset :
∀ {X : Type u_1} {R : Type u_9} {ι : Type u_10} [inst : TopologicalSpace X] {U : ι → Set X} [inst_1 : Zero R]
{f : ι → X → R},
(LocallyFinite fun i => Function.support (f i)) →
(∀ (i : ι), tsupport (f i) ⊆ U i) →
(∀ (i : ι), IsOpen (U i)) →
∀ (x : X), ∃ is, ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun i => f i z) ⊆ ↑is
This theorem states that if we have a family of functions `f`, which has locally finite support (i.e., for each point in the space, we can find a neighborhood of that point that intersects the support of only finitely many functions in the family), and each function's topological support is contained within a corresponding open set in a family of open sets `U`, then for any given point, we can find a neighborhood around that point such that only finitely many members of `f` are non-zero on this neighborhood. This neighborhood is a subset of the intersection of members of `U` corresponding to the functions with non-zero values on this neighborhood.
More concisely: Given a family of functions `f` with locally finite support and topological support contained in a corresponding family of open sets `U`, there exists a neighborhood of any point such that only finitely many functions in `f` are non-zero on the neighborhood, which is a subset of the intersection of the open sets in `U` corresponding to those functions.
|