LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

Baire category inside a closed bounded interval: if $[a,b]$ with $a < b$ is covered by a sequence of closed sets, then one of them contains a nondegenerate closed subinterval of $[a,b]$ ; no choice principle is used

Statement

Let $a, b \in \mathbb{R}$ with $a < b$ and let $(F_n)_{n \in \mathbb{N}}$ be a sequence of closed subsets of $\mathbb{R}$ (Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen) with

$[a,b] \;\subseteq\; \bigcup_{n \in \mathbb{N}} F_n$

(Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length). Then there are $n \in \mathbb{N}$ and reals $u < v$ with

$[u,v] \;\subseteq\; F_n \cap [a,b].$

No choice principle is used. The only category input is Baire category in $\mathbb{R}$ , by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $\mathbb{R}$ is not a countable union of nowhere dense sets, whose own proof selects nothing: it fixes one enumeration of the rationals and takes least indices. Nothing further is chosen below, the argument being a direct application of that theorem to the complements of the $F_n$ .

Facts & Assumptions

Given: Reals $a < b$ and a sequence $(F_n)_{n \in \mathbb{N}}$ of closed subsets of $\mathbb{R}$ with $[a,b] \subseteq \bigcup_{n} F_n$ .

[L1]

A countable intersection of dense open subsets of $\mathbb{R}$ is dense in $\mathbb{R}$ (Baire category in $\mathbb{R}$ , by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $\mathbb{R}$ is not a countable union of nowhere dense sets); dense means that the closure is $\mathbb{R}$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ).

[L2]

$\overline{S} = \mathbb{R}$ if and only if $N_\varepsilon(y) \cap S \ne \varnothing$ for every real $y$ and every real $\varepsilon > 0$ (The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points, claim 1, Interior, closure, boundary and exterior of a subset of $\mathbb{R}$ , The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ ).

[L3]

An intersection of two closed sets is closed, and the complement of a closed set is open (Arbitrary unions and finite intersections of open subsets of $\mathbb{R}$ are open, and dually for closed sets, claim 3, Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[L4]

$[a,b]$ is closed: its complement $\{x : x < a\} \cup \{x : x > b\}$ is open, since $x < a$ gives $N_{a-x}(x) \subseteq \{z : z < a\}$ and $x > b$ gives $N_{x-b}(x) \subseteq \{z : z > b\}$ (Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen, The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ , Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

$N_\varepsilon(y) = (y - \varepsilon, y + \varepsilon)$ , and for $a < b$ the midpoint $y := (a+b)/2$ and radius $\varepsilon := (b-a)/2 > 0$ give $N_\varepsilon(y) = (a,b) \subseteq [a,b]$ (The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ , Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · contradiction

1.1

Put $G_n := F_n \cap [a,b]$ for $n \in \mathbb{N}$ . Each $G_n$ is closed, being an intersection of two closed sets, and $[a,b] = \bigcup_{n} G_n$ , since $[a,b]$ is contained in the union of the $F_n$ and each $G_n$ is contained in $[a,b]$ .

L3L4

1.2

Suppose, for contradiction, that no $G_n$ contains a nondegenerate closed interval, that is, that there are no $n$ and no reals $u < v$ with $[u,v] \subseteq G_n$ .

assume-contra

2.1

Each $V_n := \mathbb{R} \setminus G_n$ is open, and it is dense. Openness is the complement of a closed set. For density, let $y$ be real and $\varepsilon > 0$ real; if $N_\varepsilon(y) \cap V_n$ were empty then $N_\varepsilon(y) \subseteq G_n$ , and then $[y - \varepsilon/2,\ y + \varepsilon/2]$ would be a nondegenerate closed interval inside $G_n$ , contrary to step 1.2.

step 1.1step 1.2L2L3L5

3.1

By the Baire category theorem the intersection $\bigcap_{n} V_n$ is dense in $\mathbb{R}$ , so it meets the neighbourhood $N_{(b-a)/2}\bigl((a+b)/2\bigr) = (a,b)$ : there is $x \in (a,b)$ with $x \notin G_n$ for every $n$ .

step 2.1L1L2L5

4.1

But $x \in (a,b) \subseteq [a,b] = \bigcup_{n} G_n$ , so $x \in G_n$ for some $n$ , contradicting step 3.1. The assumption of step 1.2 is therefore false, and some $G_n = F_n \cap [a,b]$ contains a nondegenerate closed interval $[u,v]$ .

step 1.1step 1.2step 3.1discharge-contradiction∎

Remarks

Why the statement is about $[a,b]$ and not about $\mathbb{R}$ . Baire category in $\mathbb{R}$ , by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $\mathbb{R}$ is not a countable union of nowhere dense sets says that $\mathbb{R}$ is not a countable union of nowhere dense sets. What is needed for Baire's theorem on functions of the first class (Baire's theorem: a Baire class one function on a closed bounded interval $[a,b]$ is continuous at the points of a dense subset of $[a,b]$ that is the trace of a $G_\delta$ set, so its set of discontinuities is meager) is the same statement localised to a closed bounded interval, and the localisation is not formal: a closed set may be nowhere dense in $\mathbb{R}$ and yet fill an interval, so the conclusion has to be stated as "contains a nondegenerate closed subinterval" rather than "has nonempty interior in $\mathbb{R}$ ". The two are in fact the same condition here, which is what step 2.1 uses.
The hypothesis $a < b$ is not decoration. For $a = b$ the set $[a,b]$ is a single point, it is covered by the constant sequence $F_n = \{a\}$ , and no $F_n$ contains a nondegenerate closed interval; the conclusion fails, and the proof breaks at step 3.1, where $(a,b)$ is empty.

Depends on

Used by

Baire's theorem: a Baire class one function on a closed bounded interval [a,b] is continuous at the points of a dense subset of [a,b] that is the trace of a G_δ set, so its set of discontinuities is meager Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 73 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Baire category theorem (Wikipedia) (standard reference, not scraped)

Baire category inside a closed bounded interval: if [a,b][a,b][a,b] with a<ba < ba<b is covered by a sequence of closed sets, then one of them contains a nondegenerate closed subinterval of [a,b][a,b][a,b]; no choice principle is used