Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Analytic countable operations and inclusion of Borel sets

Statement

In ZFC analytic subsets of a Polish space are closed under countable unions and countable intersections, and under continuous inverse images between Polish spaces. Every Borel set is analytic and coanalytic.

Facts & Assumptions

[F1]

Analytic and coanalytic sets by closed projection defines analytic sets as closed projections with a Baire witness and coanalytic sets by complement.

[F2]

Cantor and Baire sequence spaces and coordinate codings codes sequences of Baire witnesses by one Baire real.

[F4]

Metric Borel hierarchy inclusions and fixed-rank operations includes the rank-one to rank-two inclusion: every metric open is a countable union of closed sets.

Proof

Given: A Polish X and analytic An⊆X.

1.1F1A1

By F1 and A1 choose closed Fn⊆X×N projecting to An. For z∈N write z−=(z(1),z(2),…) and put F={(x,z):(x,z−)∈Fz(0)}. This is closed: at a point outside it, fixing z(0)=n and a product neighbourhood outside closed Fn gives a neighbourhood outside F. Its projection is ⋃nAn: a witness z gives the summand n=z(0); a witness y in a summand gives z=n⌢y. Hence the union is analytic.

1.2F1F3F5

If g:Y→X is continuous between Polish spaces and A has closed witness F, the map (y,z)↦(g(y),z) is continuous: product basic opens pull back to products of open preimages and cylinder opens. Its preimage of F is closed and projects exactly to g−1[A]. All product spaces here are Polish by F3, so F1 applies.

2.1F1F2F5A1step 1.1

Decode z as (zn)n by F2 and put H={(x,z):∀n (x,zn)∈Fn}. Each coordinate map is continuous, so its closed preimage is closed by F5 and complementation; their intersection is closed. A projected point is in every An. Conversely if x∈⋂nAn, A1 selects witnesses yn from the nonempty closed sections (Fn)x, and F2 codes them as z with (x,z)∈H. Thus this projection is exactly the intersection, analytic by F1.

3.1F1F4step 1.1step 2.1

A closed C⊆X has the closed witness C×N; this projects to C since the all-zero Baire real exists. By F4 and step 1.1 every open is analytic. Let H consist of sets both they and their complements analytic. It contains opens and is complement closed. If An∈H, step 1.1 makes their union analytic and step 2.1 makes its complement, the intersection of their analytic complements, analytic. Thus H is a sigma-algebra containing opens and contains every Borel set by the leastness definition. Empty intersections give X, and empty unions give ∅, both already supplied by the closed-witness construction. QED.

Depends on

Used by

Dependency tree · two levels

18 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