TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)

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)

[L3]

The rationals have a fixed enumeration and are dense in the reals ( $Q$ is countably infinite, Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

Proof

technique · direct

1.1L1givenalgebra

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

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})$ . Decompose each finite union into its uniquely ordered maximal h-interval components and flatten the resulting doubly indexed family. This is a canonical construction, with no countable choice. Applying the single-interval case to each $I_{r}$ and summing finitely gives the general case.

2.1step 1.1L1givenalgebra

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

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.1step 2.1L1givenalgebra

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

Let $ε > 0$ . Right continuity at $a$ gives $0 < δ < b - a$ with $F (a + δ) - F (a) < ε / 2$ . Fix one enumeration $(q_{m})_{m \geq 0}$ of $Q$ by [L3]. For each $n$ such that $I_{n}$ meets $[a + δ, b]$ , its right endpoint $v_{n}$ is finite; write $u_{n}$ for its left endpoint. Right continuity of $F$ at $v_{n}$ and density of $Q$ show that the set of indices $m$ with $q_{m} > v_{n}$ and $F (q_{m}) - F (v_{n}) < ε 2^{- n - 2}$ is nonempty. Let $w_{n}$ be $q_{m}$ for its least such index. This formula fixes all the $w_{n}$ without Countable Choice. Then the open intervals $(u_{n}, w_{n})$ cover $[a + δ, b]$ : every $x$ in that compact interval belongs to some $I_{n} \subseteq (a, b]$ , hence $u_{n} < x \leq v_{n} < w_{n}$ . [given, L2, L3, construct]

4.1step 3.1L1algebra

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

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.1step 2.1step 4.1

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

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

6.1step 2.1step 5.1algebra

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]$ .

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.1step 2.1step 5.1step 6.1algebra

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]$ .

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.1step 1.1step 5.1step 6.1step 7.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.

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

48 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)