LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A locally finite nonnegative family with positive pointwise sum normalizes to a partition of unity

Statement

Let ${f_{s} : X \to [0, \infty)}_{s \in S}$ be continuous with locally finite cozero family, and suppose $f : = \sum_{s} f_{s}$ is positive at every point. Then $φ_{s} : = f_{s} / f$ form a partition of unity; their cozero sets and supports are the same as those of the corresponding $f_{s}$ .

Facts & Assumptions

Given: A locally finite nonnegative continuous family whose pointwise sum is everywhere positive.

[L1]

The sum $f = \sum_{s} f_{s}$ is continuous (A locally finite family of continuous nonnegative functions has a continuous pointwise sum).

[L2]

A quotient of continuous real-valued maps is continuous on the cozero set of its denominator (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[F1]

A family of continuous maps $X \to [0, 1]$ is a partition of unity exactly when its cozero family is locally finite and its pointwise sum is one (Locally finite partitions of unity and subordination to an open cover).

Proof

technique · direct

1.1

By [L1] the function $f$ is continuous, and the positivity hypothesis makes $coz (f) = X$ .

2.1

Therefore each $φ_{s} = f_{s} / f$ is continuous by [L2] and nonnegative. Since $f_{s} (x) \leq f (x)$ , it takes values in $[0, 1]$ , and positivity of $f$ gives $coz (φ_{s}) = coz (f_{s})$ .

step 1.1L2

3.1

At every $x \in X$ , local finiteness makes the sum finite and gives $\sum_{s} φ_{s} (x) = \sum_{s} f_{s} (x) / f (x) = f (x) / f (x) = 1$ .

step 2.1

4.1

The cozero family is unchanged, hence locally finite, and equality of cozero sets also gives equality of supports. Thus [F1] says that ${φ_{s}}$ is a partition of unity.

step 2.1step 3.1F1∎

Depends on

Used by

Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity Theorem

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Robbin, Partitions of Unity (standard reference, not scraped)
S. Semmes, Topology notes, Sections 5.13–5.14 (Rice University) (standard reference, not scraped)