TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

The Stieltjes interval set function is a premeasure

Statement

Let $F : R \to R$ be nondecreasing and right-continuous, and let $μ_{0, F}$ be the set function of The interval set function attached to a nondecreasing right-continuous function. Then $μ_{0, F}$ is a premeasure on the half-open interval algebra in the sense of Premeasures on algebras of sets.

Facts & Assumptions

Given: A nondecreasing right-continuous function $F : R \to R$ , the associated interval set function $μ_{0, F}$ , a pairwise disjoint sequence $(E_{n})_{n \in N}$ in the half-open interval algebra, and a set $E = ⋃_{n \in N} E_{n}$ that also lies in the half-open interval algebra.

[L1]

The set function $μ_{0, F}$ is well defined and finitely additive on the half-open interval algebra. (The Stieltjes interval set function is finitely additive on the half-open interval algebra)

[L2]

Every closed bounded interval $[a, b]$ is compact. (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact)

Proof

technique · direct

1.1

By [L1], it is enough to prove countable additivity when $E$ is a single h-interval.

L1givenalgebra

Indeed, if $E = ⋃_{r = 1}^{m} I_{r}$ is a finite disjoint union of h-intervals, then each $E_{n} \cap I_{r}$ is again a finite disjoint union of h-intervals, the families $(E_{n} \cap I_{r})_{n}$ are pairwise disjoint, and $I_{r} = ⋃_{n} (E_{n} \cap I_{r})$ . Applying the single-interval case to each $I_{r}$ and summing finitely gives the general case.

2.1

Let $E = ⋃_{n} I_{n}$ be a disjoint union of h-intervals, with $E$ itself an h-interval.

step 1.1L1givenalgebra

For every $N \in N$ ,

$\sum_{n = 0}^{N} μ_{0, F} (I_{n}) = μ_{0, F} ⁣ (⋃_{n = 0}^{N} I_{n}) \leq μ_{0, F} (E),$

because $E$ is the disjoint union of $⋃_{n = 0}^{N} I_{n}$ and the remainder $E ∖ ⋃_{n = 0}^{N} I_{n}$ , whose $μ_{0, F}$ -value is nonnegative. Hence $\sum_{n} μ_{0, F} (I_{n}) \leq μ_{0, F} (E)$ . [step 1.1, L1, given, algebra]

3.1

Assume first that $E = (a, b] = ⋃_{n \in N} I_{n}$ , where the $I_{n}$ are pairwise disjoint h-intervals.

step 2.1L1givenalgebra

Let $ε > 0$ . Right continuity at $a$ gives $δ > 0$ with $F (a + δ) - F (a) < ε / 2$ . For each $n$ , if $I_{n}$ meets $[a + δ, b]$ then its right endpoint is finite; write that endpoint as $v_{n}$ , let $u_{n}$ be its left endpoint, and choose $w_{n} > v_{n}$ with $F (w_{n}) - F (v_{n}) < ε 2^{- n - 2}$ . Then the open intervals $(u_{n}, w_{n})$ cover $[a + δ, b]$ : every $x$ in that compact interval belongs to $⋃_{n} I_{n} = (a, b]$ , hence lies in some $I_{n}$ that must have finite right endpoint and therefore satisfies $x \in (u_{n}, w_{n})$ . [given, L2, choose]

4.1

By compactness from [L2], finitely many of those open intervals cover $[a + δ, b]$ .

step 3.1L1algebra

Write them as $(u_{n_{1}}, w_{n_{1}}), \dots, (u_{n_{m}}, w_{n_{m}})$ . Since $(a + δ, b] \subseteq ⋃_{j = 1}^{m} (u_{n_{j}}, w_{n_{j}}]$ , monotonicity and finite additivity give

$F (b) - F (a + δ) \leq \sum_{j = 1}^{m} (F (w_{n_{j}}) - F (u_{n_{j}})) < \sum_{j = 1}^{m} μ_{0, F} (I_{n_{j}}) + \frac{ε}{2} \leq \sum_{n} μ_{0, F} (I_{n}) + \frac{ε}{2} .$

Adding $F (a + δ) - F (a) < ε / 2$ yields

$F (b) - F (a) < \sum_{n} μ_{0, F} (I_{n}) + ε .$

[step 2.1, step 3.1, L1, algebra]

5.1

Because $ε > 0$ was arbitrary, step 4.1 gives $μ_{0, F} ((a, b]) \leq \sum_{n} μ_{0, F} (I_{n})$ .

step 2.1step 4.1

Together with step 2.1, this proves countable additivity for bounded intervals. [step 2.1, step 4.1]

6.1

If $E = (- \infty, b]$ , then for every real $M < b$ the bounded interval $(M, b]$ is the disjoint union of the h-intervals $I_{n} \cap (M, b]$ .

step 2.1step 5.1algebra

By step 5.1,

$F (b) - F (M) = \sum_{n} μ_{0, F} (I_{n} \cap (M, b]) \leq \sum_{n} μ_{0, F} (I_{n}) .$

Taking the supremum over $M < b$ gives $μ_{0, F} (E) \leq \sum_{n} μ_{0, F} (I_{n})$ . Combined with step 2.1, this proves countable additivity for left rays. The same argument with $(a, M]$ proves the right-ray case $E = (a, \infty)$ . [step 2.1, step 5.1, algebra]

7.1

If $E = R$ , then for every real $M < N$ the bounded interval $(M, N]$ is the disjoint union of the h-intervals $I_{n} \cap (M, N]$ .

step 2.1step 5.1step 6.1algebra

So step 5.1 gives

$F (N) - F (M) = \sum_{n} μ_{0, F} (I_{n} \cap (M, N]) \leq \sum_{n} μ_{0, F} (I_{n}) .$

Taking the supremum over $M < N$ yields $μ_{0, F} (R) \leq \sum_{n} μ_{0, F} (I_{n})$ . Together with step 2.1 and step 6.1, this proves countable additivity for every h-interval. [step 2.1, step 5.1, step 6.1, algebra]

8.1

By step 1.1, the single-interval cases of steps 5.1 through 7.1 imply the general countable additivity clause whenever a disjoint union in the algebra stays in the algebra.

step 1.1step 5.1step 6.1step 7.1

Therefore $μ_{0, F}$ is a premeasure. [step 1.1, step 5.1, step 6.1, step 7.1] ∎

Depends on

Used by

Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on ℝ Theorem

Dependency tree · two levels

25 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

Gerald B. Folland, Real Analysis, 2nd ed., Proposition 1.15 (standard reference, not scraped)