Description: The other half of rpnnen , where we show an injection from sets of positive integers to real numbers. The obvious choice for this is binary expansion, but it has the unfortunate property that it does not produce an injection on numbers which end with all 0's or all 1's (the more well-known decimal version of this is 0.999... ). Instead, we opt for a ternary expansion, which produces (a scaled version of) the Cantor set. Since the Cantor set is riddled with gaps, we can show that any two sequences that are not equal must differ somewhere, and when they do, they are placed a finite distance apart, thus ensuring that the map is injective.
Our map assigns to each subset A of the positive integers the number sum_ k e. A ( 3 ^ -u k ) = sum_ k e. NN ( ( FA )k ) , where ( ( FA )k ) = if ( k e. A , ( 3 ^ -u k ) , 0 ) ) ( rpnnen2lem1 ). This is an infinite sum of real numbers ( rpnnen2lem2 ), and since A C_ B implies ( FA ) <_ ( FB ) ( rpnnen2lem4 ) and ( FNN ) converges to 1 / 2 ( rpnnen2lem3 ) by geoisum1 , the sum is convergent to some real ( rpnnen2lem5 and rpnnen2lem6 ) by the comparison test for convergence cvgcmp . The comparison test also tells us that A C_ B implies sum_ ( FA ) <_ sum_ ( FB ) ( rpnnen2lem7 ).
Putting it all together, if we have two sets x =/= y , there must differ somewhere, and so there must be an m such that A. n < m ( n e. x <-> n e. y ) but m e. ( x \ y ) or vice versa. In this case, we split off the first m - 1 terms ( rpnnen2lem8 ) and cancel them ( rpnnen2lem10 ), since these are the same for both sets. For the remaining terms, we use the subset property to establish that sum_ ( Fy ) <_ sum_ ( F( NN \ { m } ) ) and sum_ ( F{ m } ) <_ sum_ ( Fx ) (where these sums are only over ( ZZ>=m ) ), and since sum_ ( F( NN \ { m } ) ) = ( 3 ^ -u m ) / 2 ( rpnnen2lem9 ) and sum_ ( F{ m } ) = ( 3 ^ -u m ) , we establish that sum_ ( Fy ) < sum_ ( Fx ) ( rpnnen2lem11 ) so that they must be different. By contraposition ( rpnnen2lem12 ), we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013) (Proof shortened by Mario Carneiro, 30-Apr-2014) (Revised by NM, 17-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rpnnen2 | ⊢ 𝒫 ℕ ≼ ( 0 [,] 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | ⊢ ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ) = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ) | |
| 2 | 1 | rpnnen2lem12 | ⊢ 𝒫 ℕ ≼ ( 0 [,] 1 ) |