Theorems · Definition · general topology

BumpCovering.toPartitionOfUnity

{ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → PartitionOfUnity ι X s

The partition of unity defined by a BumpCovering. The partition of unity is given by the formula g i x = f i x * ∏ᶠ j < i, (1 - f j x). In other words, g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x), so ∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x). If x ∈ s, then one of f j x equals one, hence the product of 1 - f j x vanishes, and ∑ᶠ i, g i x = 1. In order to avoid an assumption LinearOrder ι, we use WellOrderingRel instead of (<).

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

14 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace