LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\varphi_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 $\operatorname{coz}(f)=X$ .

2.1

Therefore each $\varphi_s=f_s/f$ is continuous by [L2] and nonnegative. Since $f_s(x)\le f(x)$ , it takes values in $[0,1]$ , and positivity of $f$ gives $\operatorname{coz}(\varphi_s)=\operatorname{coz}(f_s)$ .

step 1.1L2

3.1

At every $x\in X$ , local finiteness makes the sum finite and gives $\sum_s\varphi_s(x)=\sum_sf_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 $\{\varphi_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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 46 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)