PartitionOfUnity.exists_isSubordinate
theorem PartitionOfUnity.exists_isSubordinate :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X]
[inst_2 : ParacompactSpace X],
IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
The theorem `PartitionOfUnity.exists_isSubordinate` states that for any type `ι` and topological space `X`, if `X` is a normal and paracompact space, then for any closed set `s` and an open cover `U` of `s` indexed by `ι`, there exists a partition of unity `f` subordinate to `U`. Here, "partition of unity" is a concept from topology that refers to a collection of continuous functions whose values are always non-negative and sum to 1 at each point in a topological space. The concept of "subordinate" in this context means that the support of each function in the partition of unity is contained in a set from the open cover `U`.
More concisely: In a normal and paracompact topological space, for any closed set and open cover, there exists a partition of unity with supports contained in the cover.
|
BumpCovering.locallyFinite
theorem BumpCovering.locallyFinite :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s),
LocallyFinite fun i => Function.support ⇑(f i)
The theorem `BumpCovering.locallyFinite` states that for any type `ι`, any topological space `X`, and any set `s` of `X`, if `f` is a bump covering (a mathematical tool often used in differential geometry) of `s` indexed by `ι`, then the family of supports of the functions of `f` is locally finite. In other words, for every point in the topological space, there exists a neighborhood of that point that intersects with the support of only finitely many functions from the bump covering.
More concisely: Given a bump covering `f` of a set `s` in a topological space `X` indexed by type `ι`, the family of supports of its functions is locally finite.
|
PartitionOfUnity.exists_pos
theorem PartitionOfUnity.exists_pos :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X},
x ∈ s → ∃ i, 0 < (f i) x
The theorem `PartitionOfUnity.exists_pos` states that if `f` is a partition of unity over a set `s` in a topological space `X`, then for every element `x` that belongs to `s`, there exists an index `i` such that the value of `f` at index `i` and at `x` is greater than zero. A partition of unity is a mathematical tool used in areas such as differential geometry and topology to "stitch" together local information into a global result.
More concisely: For every element x in a set s of a topological space X with respect to a partition of unity f, there exists an index i such that f i(x) > 0.
|
BumpCovering.IsSubordinate.toPartitionOfUnity
theorem BumpCovering.IsSubordinate.toPartitionOfUnity :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ι → Set X},
f.IsSubordinate U → f.toPartitionOfUnity.IsSubordinate U
The theorem `BumpCovering.IsSubordinate.toPartitionOfUnity` states that for any type `ι`, any type `X` with a topological space structure, any set `s` of type `X`, any bump covering `f` of type `BumpCovering ι X s`, and any family of sets `U` indexed by `ι`, if the bump covering `f` is subordinate to the family of sets `U` (meaning that for each index `i`, the closure of the support of `f i` is a subset of `U i`), then the partition of unity obtained from the bump covering `f` (denoted `BumpCovering.toPartitionOfUnity f`) is also subordinate to the same family of sets `U`.
More concisely: If a bump covering is subordinate to a family of sets, then the partition of unity obtained from the bump covering is also subordinate to the same family.
|
BumpCovering.exists_isSubordinate
theorem BumpCovering.exists_isSubordinate :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X]
[inst_2 : ParacompactSpace X],
IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
The theorem `BumpCovering.exists_isSubordinate` states that for any types `ι` and `X` with `X` being a topological space, a set `s` of type `X`, and `X` being a normal space and a paracompact space, if `s` is a closed set and `U` is a function from `ι` to open sets in `X` such that `s` is a subset of the union of these open sets, then there exists a bump covering of `s` in `X` that is subordinate to `U`. A bump covering is a family of smooth functions which can be used to partition unity.
More concisely: Given a normal and paracompact topological space `X` with a closed subset `s` and a collection `U` of open sets in `X` such that `s` is a subset of the union of `U`, there exists a subordinate bump covering for `s` in `X`.
|
PartitionOfUnity.sum_eq_one
theorem PartitionOfUnity.sum_eq_one :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X},
x ∈ s → (finsum fun i => (f i) x) = 1
This theorem states that for any type `ι`, any topological space `X`, any set `s` of `X`, any partition of unity `f` over `ι`, `X`, and `s`, and any element `x` of `X`, if `x` is in `s`, then the finite sum of `(f i) x` over all `i` equals 1. Essentially, for any point `x` in the domain of a partition of unity, the sum of the functions at that point is equal to 1. Here, a partition of unity is a collection of continuous functions (from the space to the real numbers) that are positive, have support that is compact (i.e., closed and bounded), and the sum of which is always 1 at any point in the space.
More concisely: For any topological space X, partition of unity f over X and ι, and x ∈ X belonging to the union of supports of f i, the sum ∑ i:ι (f i x) equals 1.
|
PartitionOfUnity.nonneg
theorem PartitionOfUnity.nonneg :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X),
0 ≤ (f i) x
This theorem states that, for any types `ι` and `X`, with `X` being a topological space, and for any set `s` of elements from `X`, if `f` is a partition of unity indexed by `ι` over `X` restricted to `s`, then each function `f i` in the partition, evaluated at any point `x` in `X`, is non-negative. In simpler terms, all function values in a partition of unity of a topological space are non-negative.
More concisely: For any topological space X and indexed family f i : ι → C^0(X) of continuous real-valued functions on X forming a partition of unity, ∀ i ∈ ι, ∀ x ∈ X, f i x ≥ 0.
|
PartitionOfUnity.exists_isSubordinate_of_locallyFinite
theorem PartitionOfUnity.exists_isSubordinate_of_locallyFinite :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X],
IsClosed s →
∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
This theorem states that if `X` is a normal topological space and `U` is an open covering of a closed set `s` that is locally finite, then there exists a partition of unity `f` that is subordinate to `U` on `s`. Here, a covering `U` of a set `s` is said to be locally finite if, at every point in `X`, there is a neighborhood that intersects with only finitely many sets from `U`. A partition of unity `f` is said to be subordinate to `U` if each function in the partition is supported on some set from `U`. If `X` is also paracompact, the assumption that `U` is locally finite can be omitted.
More concisely: If `X` is a normal and paracompact topological space, and `U` is an open covering of a closed set `s` in `X`, then there exists a partition of unity `f` subordinate to `U` on `s`.
|
PartitionOfUnity.continuous_finsum_smul
theorem PartitionOfUnity.continuous_finsum_smul :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
[inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul ℝ E] {s : Set X}
(f : PartitionOfUnity ι X s) [inst_5 : ContinuousAdd E] {g : ι → X → E},
(∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContinuousAt (g i) x) → Continuous fun x => finsum fun i => (f i) x • g i x
The theorem `PartitionOfUnity.continuous_finsum_smul` states that if `f` is a partition of unity on a set `s` of type `X` (meaning `f` is a collection of functions that sum to one at every point in `s`), and there is a family of functions `g : ι → X → E` such that each function `g i` is continuous at every point of the topological support of `f i` (the closure of the set of points where `f i` is non-zero), then the function that maps `x` to the finite sum of `f i x` times `g i x` over `i` is continuous over the whole space. This theorem is true in a topological space `X` and a topological vector space `E` over the real numbers, where the addition operation in `E` is continuous and the scalar multiplication operation in `E` is continuous and commutative.
More concisely: If `f` is a partition of unity on a set `s` in a topological space `X` and each `g i` is continuous on the topological support of `f i` in a topological vector space `E` over the real numbers, then the function that maps `x` to the finite sum of `f i x` times `g i x` over `i` is continuous on `X`.
|
PartitionOfUnity.mem_finsupport
theorem PartitionOfUnity.mem_finsupport :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) {i : ι},
i ∈ ρ.finsupport x₀ ↔ i ∈ Function.support fun i => (ρ i) x₀
This theorem states that for any type `ι`, topological space `X`, set `s` of `X`, partition of unity `ρ` on `s` indexed by `ι`, and point `x₀` in `X`, a given index `i` of type `ι` is in the finitely supported partition of unity at `x₀` if and only if `i` exists in the support of the function obtained by applying partition of unity `ρ` at `x₀`. This essentially relates the support of a partition of unity at a point to the support of the corresponding function over the indices.
More concisely: For any type `ι`, topological space `X`, set `s` of `X`, partition of unity `ρ` on `s` indexed by `ι`, and point `x₀` in `X`, an index `i` of type `ι` is in the finitely supported partition of unity at `x₀` if and only if `i` is in the support of the function `ρ(x₀)`.
|
PartitionOfUnity.locallyFinite
theorem PartitionOfUnity.locallyFinite :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s),
LocallyFinite fun i => Function.support ⇑(f i)
The theorem `PartitionOfUnity.locallyFinite` states that for any type `ι`, any topological space `X`, and any set `s : Set X`, given a partition of unity `f` indexed by `ι` on the set `s`, the family of supports of the functions `(f i)`, where `i` ranges over the index set `ι`, is locally finite. In other words, for every point `x` in the topological space `X`, there exists a neighborhood of `x` that intersects the support of only finitely many functions in the partition of unity.
More concisely: Given a topological space X, a type ι, a set s : Set X, and a partition of unity f indexed by ι on s, the family of supports of the functions (fi) has locally finite intersection with every neighborhood in X.
|
PartitionOfUnity.continuous_smul
theorem PartitionOfUnity.continuous_smul :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
[inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul ℝ E] {s : Set X}
(f : PartitionOfUnity ι X s) {g : X → E} {i : ι},
(∀ x ∈ tsupport ⇑(f i), ContinuousAt g x) → Continuous fun x => (f i) x • g x
The theorem `PartitionOfUnity.continuous_smul` states that given a partition of unity `f` on a set `s` of a topological space `X`, and a function `g : X → E` that is continuous at every point of the topological support of any `f i`, then the function defined as `x ↦ f i x • g x` is continuous on the whole space. Here `E` is an additive commutative monoid with zero multiplication that is also a topological space which possesses the property of continuous scalar multiplication by real numbers. A partition of unity is typically a collection of continuous functions on a topological space that sum up to one at each point. The topological support of a function is the closure of the set of points where the function is non-zero.
More concisely: Given a partition of unity `f` on a topological space `X` and a continuous function `g` on the topological support of each `f i`, the function `x ↦ Σ(fi x * g x)` is continuous on `X`. (Here, `Σ` denotes the sum over the index set of the partition of unity.)
|
BumpCovering.exists_isSubordinate_of_prop
theorem BumpCovering.exists_isSubordinate_of_prop :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X]
[inst_2 : ParacompactSpace X] (p : (X → ℝ) → Prop),
(∀ (s t : Set X),
IsClosed s →
IsClosed t →
Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
IsClosed s →
∀ (U : ι → Set X),
(∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
The theorem `BumpCovering.exists_isSubordinate_of_prop` states that for any types `ι` and `X`, where `X` is equipped with a topological space structure, a closed subset `s` of `X`, and `X` is a normal and paracompact space, given a predicate `p` on functions from `X` to real numbers, if for any two closed and disjoint subsets `s` and `t` of `X`, there exists a function `f` such that `p` holds on `f`, `f` is zero on `s`, `f` is one on `t`, and the value of `f` at any point `x` lies in the closed interval from 0 to 1, then if `s` is closed and `U` is a family of open subsets of `X` that covers `s`, there exists a `BumpCovering` `f` such that the predicate `p` holds on each function of the covering and `f` is subordinate to `U`.
In simpler terms, this theorem says that under certain conditions, there exists a smooth partition of unity subordinate to a given open cover that satisfies a given property. This is often used in manifold theory, where it guarantees the ability to glue together locally defined objects into a globally defined object.
More concisely: Given a normal and paracompact topological space `X` with a closed subset `s`, a predicate `p` on functions from `X` to real numbers, and an open cover `U` of `s`, if for any pair of disjoint closed subsets of `X`, there exists a function `f` satisfying `p(f)` and `f` is zero on one subset, one on the other, and takes values in [0,1], then there exists a `BumpCovering` `f` of `U` such that `p(f)` holds for each function in the covering.
|
PartitionOfUnity.IsSubordinate.continuous_finsum_smul
theorem PartitionOfUnity.IsSubordinate.continuous_finsum_smul :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
[inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousSMul ℝ E] {s : Set X}
{f : PartitionOfUnity ι X s} [inst_5 : ContinuousAdd E] {U : ι → Set X},
(∀ (i : ι), IsOpen (U i)) →
f.IsSubordinate U →
∀ {g : ι → X → E},
(∀ (i : ι), ContinuousOn (g i) (U i)) → Continuous fun x => finsum fun i => (f i) x • g i x
This theorem states that given a topological space `X`, a set `s` in `X`, a partition of unity `f` over `X` subordinate to a family of open sets `U i`, and a family of functions `g : ι → X → E` such that each `g i` is continuous on `U i`, the sum function `fun x ↦ ∑ᶠ i, f i x • g i x` is a continuous function.
In other words, under these conditions, the weighted sum of the functions in the family `g`, where the weights are given by the partition of unity `f`, yields a continuous function. Here `∑ᶠ i` denotes finite sum over `i`, `f i x` is the value of `f` at index `i` and `x`, and `f i x • g i x` represents the scaled function `g i x` by the factor `f i x`.
More concisely: Given a topological space X, a partition of unity f over X subordinate to a family of open sets U i, and a family of continuous functions g i : X -> E indexed by I, the function x => ∑ᶠ i, f i x * g i x is continuous.
|
BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop
theorem BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X] (p : (X → ℝ) → Prop),
(∀ (s t : Set X),
IsClosed s →
IsClosed t →
Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
IsClosed s →
∀ (U : ι → Set X),
(∀ (i : ι), IsOpen (U i)) →
LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
This theorem states that for a normal topological space `X` and a closed set `s` in `X`, if `U i`, for `i` in some index set `ι`, is a locally finite open covering of `s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. A `BumpCovering` is a collection of bump functions, which are smooth functions that are zero outside a given set. The BumpCovering will satisfy a predicate `p` which aligns with Urysohn's lemma, meaning there exists such a function `f` where `p ⇑f` holds and `⇑f` maps to `0` on `s` and `1` on `t` for any disjoint closed sets `s` and `t`, with all function values in the interval `[0, 1]`. This theorem also states that if `X` is a paracompact space, the assumption of local finiteness of `U` can be omitted.
More concisely: Given a normal topological space `X`, a closed set `s`, and a locally finite open covering `{U i}_{i ∈ ι}` of `s`, there exists a subordinate `BumpCovering ι X s` satisfying the Urysohn lemma predicate. If `X` is paracompact, local finiteness is not required.
|
PartitionOfUnity.coe_finsupport
theorem PartitionOfUnity.coe_finsupport :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
↑(ρ.finsupport x₀) = Function.support fun i => (ρ i) x₀
This theorem states that for a given partition of unity `ρ` on a set `s` in a topological space `X` and for a point `x₀` in `X`, the finite support of the partition of unity at `x₀` is equal to the set of indices `i` such that `(ρ i) x₀ ≠ 0`. In other words, `i` belongs to the finite support of `ρ` at `x₀` if and only if the value of the `i`-th function of the partition at `x₀` is non-zero.
More concisely: For a partition of unity `ρ` on a set `s` in a topological space `X` and a point `x₀` in `X`, the finite support of `ρ` at `x₀` equals the set of indices `i` where `(ρ i) x₀` is non-zero.
|
BumpCovering.exists_isSubordinate_of_locallyFinite
theorem BumpCovering.exists_isSubordinate_of_locallyFinite :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [inst_1 : NormalSpace X],
IsClosed s →
∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
The theorem `BumpCovering.exists_isSubordinate_of_locallyFinite` states that for any type `ι` and a type `X` endowed with a topology and a normal space structure, given a closed set `s` in `X` and a family of sets `U` indexed by `ι` such that each `U i` is open and the family `U` is locally finite, if `s` is a subset of the union of all `U i`, then there exists a bump covering `f` of `s` that is subordinate to `U`. If `X` is also a paracompact space, then the condition that the family `U` is locally finite can be omitted, as described in `BumpCovering.exists_isSubordinate`.
This theorem is a part of the theory of topological spaces, particularly dealing with the properties of normal and paracompact spaces. A bump covering is a specific type of covering of a subset of a topological space, and a bump covering being subordinate to a family of sets essentially means that the support of each function in the bump covering is contained in the corresponding set from the family.
More concisely: Given a normal or paracompact space `X` with topology, a closed set `s`, and a locally finite open cover `U`, if `s` is a subset of the union of all `U i`, then there exists a bump covering `f` of `s` that is subordinate to `U`.
|
BumpCovering.sum_toPOUFun_eq
theorem BumpCovering.sum_toPOUFun_eq :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X),
(finsum fun i => f.toPOUFun i x) = 1 - finprod fun i => 1 - (f i) x
The theorem `BumpCovering.sum_toPOUFun_eq` states that for any topological space `X`, a set `s` of `X`, and a function `f` representing a bump covering of the set `s`, for any element `x` of `X`, the sum over all `i` of the `i`-th partition of unity function of `f` evaluated at `x` is equal to 1 minus the product over all `i` of 1 minus the `i`-th bump function of `f` evaluated at `x`. In other words, it describes a relationship between the sum of partition of unity functions and the product of bump functions in a bump covering of a topological space.
More concisely: For any topological space X, set s, and bump covering function f, the sum over i of the i-th partition of unity function of f evaluated at x equals 1 minus the product over i of 1 minus the i-th bump function of f evaluated at x.
|