Theorems · Inductive type · general topology

BumpCovering

Type u_1 → (X : Type u_2) → [TopologicalSpace X] → optParam (Set X) Set.univ → Type (max u_1 u_2)

A BumpCovering ι X s is an indexed family of functions f i, i : ι, such that * the supports of f i form a locally finite family of sets, i.e., for every point x : X there exists a neighborhood U ∋ x such that all but finitely many functions f i are zero on U; * for all i, x we have 0 ≤ f i x ≤ 1; * each point x ∈ s belongs to the interior of {x | f i x = 1} for some i. One of the main use cases for a BumpCovering is to define a PartitionOfUnity, see BumpCovering.toPartitionOfUnity, but some proofs can directly use a BumpCovering instead of a PartitionOfUnity. If X is a normal paracompact space, then BumpCovering.exists_isSubordinate guarantees that for every open covering U : Set (Set X) of s there exists a BumpCovering of s that is subordinate to U.

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

46 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpace