DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 outer set function induced by a premeasure

Definition

Let $μ_{0}$ be a premeasure on an algebra $A_{0}$ of subsets of $X$ . The set function induced by $μ_{0}$ assigns $E \subseteq X$ the infimum of $\sum_{k} μ_{0} (A_{k})$ over all countable algebra covers $E \subseteq ⋃_{k} A_{k}$ . In symbols,

$μ^{*} (E) : = \inf {\sum_{k = 0}^{\infty} μ_{0} (A_{k}) : A_{k} \in A_{0} and E \subseteq ⋃_{k \in N} A_{k}} .$

The family of covering costs is nonempty because $X \in A_{0}$ and $(X, \emptyset, \emptyset, \dots)$ covers every $E$ . It therefore has an infimum in $[0, + \infty]$ by completeness of the extended real line (Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ ). This definition calls $μ^{*}$ an outer set function until its outer-measure axioms have been proved.

The outer set function induced by a premeasure

Definition

Depends on

Dependency tree · 2 levels

Sources