Theorem 10.8 — partitions of unity

Proved

Rudin.ch10_partition_of_unity

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysistopology

Let $K$ be a compact subset of $\mathbb{R}^n$ covered by open sets $V_\alpha$ . Then there are finitely many continuous functions $\psi_1,\dots,\psi_s$ with compact support, each supported in some $V_\alpha$ , with $\psi_j \ge 0$ , $\sum_j \psi_j = 1$ on $K$ , and $\sum_j \psi_j \le 1$ everywhere.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.8 (partitions of unity): if `K` is a compact subset of `ℝⁿ` covered by
open sets `V i`, there are finitely many continuous functions `ψ j` with compact support, each
supported in one of the `V i`, with `0 ≤ ψ j`, `∑ ψ j = 1` on `K` and `∑ ψ j ≤ 1`
everywhere. -/
theorem ch10_partition_of_unity (n : ℕ) (K : Set (Fin n → ℝ)) (hK : IsCompact K)
    (ι : Type) (V : ι → Set (Fin n → ℝ)) (hV : ∀ i, IsOpen (V i)) (hcover : K ⊆ ⋃ i, V i) :
    ∃ (s : ℕ) (ψ : Fin s → (Fin n → ℝ) → ℝ) (idx : Fin s → ι),
      (∀ j, Continuous (ψ j)) ∧ (∀ j, ∀ x, 0 ≤ ψ j x) ∧
      (∀ j, HasCompactSupport (ψ j)) ∧ (∀ j, tsupport (ψ j) ⊆ V (idx j)) ∧
      (∀ x ∈ K, ∑ j, ψ j x = 1) ∧ (∀ x, ∑ j, ψ j x ≤ 1) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10, p. 251, Theorem 10.8

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $n \in \mathbb{N}$ , let $K \subseteq \mathbb{R}^n$ be compact, let $\iota$ be an arbitrary index type in the lowest universe and $V : \iota \to \mathcal{P}(\mathbb{R}^n)$ a family of open sets with $K \subseteq \bigcup_i V_i$ . Then there exist a natural number $s$ , functions $\psi_0,\dots,\psi_{s-1} : \mathbb{R}^n\to\mathbb{R}$ , and an assignment $\mathrm{idx} : \{0,\dots,s-1\} \to \iota$ , such that:

each $\psi_j$ is continuous on all of $\mathbb{R}^n$ ;
$\psi_j(x) \ge 0$ for every $j$ and every $x$ ;
each $\psi_j$ has compact support;
the closed support of $\psi_j$ is contained in $V_{\mathrm{idx}(j)}$ ;
$\sum_{j} \psi_j(x) = 1$ for every $x \in K$ ;
$\sum_{j} \psi_j(x) \le 1$ for every $x \in \mathbb{R}^n$ .

The family is finite (indexed by $\{0,\dots,s-1\}$ ), and $s = 0$ is allowed — which can only occur when $K$ is empty. Smoothness of the $\psi_j$ is not asserted, only continuity.

Human review

Endorsed by Shuze Chen · Sep 14, 2026
Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph