Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

If μ is sigma-finite and A is countably generated, then Lp(μ) is separable for 1≤p<∞

Statement

Assume the Axiom of Countable Choice.

Let (X,A,μ) be a sigma-finite measure space with countably generated sigma-algebra, and let 1≤p<∞. Then Lp(μ) is separable.

Facts & Assumptions

Given: The Axiom of Countable Choice, a sigma-finite countably generated measure space, and an exponent 1≤p<∞.

[L1]

Simple functions with finite-measure support are dense in Lp(μ) (Simple functions with finite-measure support are dense in Lp(μ) for 1≤p<∞).

[L3]

The quotient Lp(μ) is the space in question, and separability means the existence of a countable dense subset (The space Lp(μ) as the quotient by null functions, Separability: the existence of an at most countable dense subset).

Proof

technique · direct
1.1L2L3givenalgebra

Let A0 be the countable algebra from [L2], and let S [L2, L3, given, algebra] be the set of all finite linear combinations ∑j=1mqj 1Aj with qj∈Q(i) and Aj∈A0 satisfying μ(Aj)<∞ for every j. Because both the coefficient set and the finite-measure members of A0 are countable, S is countable.

1.2L1L2givenchoosealgebra

To prove density, start with f∈Lp(μ) and ε>0. By [L1, L2, given, choose, algebra] [L1], choose a finite-support simple function s=∑j=1mcj 1Ej with ∥f−s∥p<ε/2. For each j, [L2] gives Aj∈A0 with μ(Aj)<∞ and μ(Ej△Aj) arbitrarily small, and each coefficient cj can be approximated by qj∈Q(i). The resulting t:=∑jqj1Aj lies in S and satisfies ∥s−t∥p<ε/2.

2.1L3step 1.1step 1.2∎

Then [L3, step 1.1, step 1.2] ∥f−t∥p≤∥f−s∥p+∥s−t∥p<ε. So S is countable and dense in Lp(μ); by [L3], the space is separable.

Depends on

Used by

Dependency tree · two levels

24 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