Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-27
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 Cantor middle-thirds set as the intersection of the sets CnC_n obtained by removing open middle thirds

Definition

For SRS \subseteq \mathbb{R} write

13S  :=  {x31:xS},23+13S  :=  {231+x31:xS},\tfrac{1}{3} S \;:=\; \{\, x \cdot 3^{-1} : x \in S \,\}, \qquad \tfrac{2}{3} + \tfrac{1}{3} S \;:=\; \{\, 2 \cdot 3^{-1} + x \cdot 3^{-1} : x \in S \,\},

and let F:P(R)P(R)F : \mathcal{P}(\mathbb{R}) \to \mathcal{P}(\mathbb{R}) be

F(S)  :=  13S  (23+13S).F(S) \;:=\; \tfrac{1}{3} S \ \cup \ \big(\tfrac{2}{3} + \tfrac{1}{3} S\big).

By the recursion theorem (The recursion theorem), applied to the set P(R)\mathcal{P}(\mathbb{R}), the starting element [0,1][0,1] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length) and the function FF, there is a unique family (Cn)nN(C_n)_{n \in \mathbb{N}} of subsets of R\mathbb{R} with

C0=[0,1],Cn+1=F(Cn)=13Cn(23+13Cn)(nN).C_0 = [0,1], \qquad C_{n+1} = F(C_n) = \tfrac{1}{3}C_n \cup \big(\tfrac{2}{3} + \tfrac{1}{3}C_n\big) \quad (n \in \mathbb{N}).

The Cantor middle-thirds set is

C  :=  nNCn.C \;:=\; \bigcap_{n \in \mathbb{N}} C_n .

The first step really is the removal of the open middle third. Directly from the clauses,

C1  =  13[0,1](23+13[0,1])  =  [0,13][23,1]  =  [0,1](13,23),C_1 \;=\; \tfrac{1}{3}[0,1] \cup \big(\tfrac{2}{3} + \tfrac{1}{3}[0,1]\big) \;=\; [0, \tfrac13] \cup [\tfrac23, 1] \;=\; [0,1] \setminus (\tfrac13, \tfrac23),

the middle equality because xx31x \mapsto x \cdot 3^{-1} is an order isomorphism of R\mathbb{R} onto itself with inverse x3xx \mapsto 3x (Ordered field, Sign rules for products and monotonicity of multiplication), and the last because 0x10 \le x \le 1 splits, by totality of the order, into x13x \le \tfrac13, 13<x<23\tfrac13 < x < \tfrac23 and x23x \ge \tfrac23. The recursion then performs the same operation inside each of the two scaled copies, which is what "removing the open middle thirds" names.

Every CnC_n lies in [0,1][0,1], by induction on nn (The principle of mathematical induction): C0=[0,1]C_0 = [0,1]; and if Cn[0,1]C_n \subseteq [0,1] then 13Cn[0,13]\tfrac13 C_n \subseteq [0,\tfrac13] and 23+13Cn[23,1]\tfrac23 + \tfrac13 C_n \subseteq [\tfrac23, 1], so Cn+1[0,1]C_{n+1} \subseteq [0,1] (Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication). The same computation shows that the two halves of Cn+1C_{n+1} are disjoint, the first lying in [0,13][0,\tfrac13] and the second in [23,1][\tfrac23,1], and 13<23\tfrac13 < \tfrac23 (The multiplicative identity is positive).

The family is nested, Cn+1CnC_{n+1} \subseteq C_n for every nn, again by induction. For n=0n = 0 this is C1=[0,13][23,1][0,1]C_1 = [0,\tfrac13] \cup [\tfrac23,1] \subseteq [0,1]. And FF is monotone, in the sense that STS \subseteq T implies F(S)F(T)F(S) \subseteq F(T), directly from the displayed description of FF; so Cn+1CnC_{n+1} \subseteq C_n gives Cn+2=F(Cn+1)F(Cn)=Cn+1C_{n+2} = F(C_{n+1}) \subseteq F(C_n) = C_{n+1}. Consequently C=nCnCmC = \bigcap_n C_n \subseteq C_m for every mm, and nCn+1=nCn=C\bigcap_n C_{n+1} = \bigcap_n C_n = C.

Powers. Here 3n3^{-n} means (31)n(3^{-1})^n, the integer power of Integer powers ama^m, so that 30=13^{0} = 1, 3(n+1)3=3n3^{-(n+1)} \cdot 3 = 3^{-n} and 3n>03^{-n} > 0 for every nn (Laws of integer exponents, Complete ordered field (least-upper-bound property)).

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 results over 17 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