Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-inp | Unicode version |
Description: Define the set of
positive reals. A "Dedekind cut" is a partition of
the positive rational numbers into two classes such that all the numbers
of one class are less than all the numbers of the other.
Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers. A Dedekind cut is an ordered pair of a lower set and an upper set which is inhabited ( ), rounded ( and likewise for ), disjoint ( ) and located ( ). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts. (Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.) |
Ref | Expression |
---|---|
df-inp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnp 7067 | . 2 | |
2 | vl | . . . . . . . 8 | |
3 | 2 | cv 1315 | . . . . . . 7 |
4 | cnq 7056 | . . . . . . 7 | |
5 | 3, 4 | wss 3041 | . . . . . 6 |
6 | vu | . . . . . . . 8 | |
7 | 6 | cv 1315 | . . . . . . 7 |
8 | 7, 4 | wss 3041 | . . . . . 6 |
9 | 5, 8 | wa 103 | . . . . 5 |
10 | vq | . . . . . . . 8 | |
11 | 10, 2 | wel 1466 | . . . . . . 7 |
12 | 11, 10, 4 | wrex 2394 | . . . . . 6 |
13 | vr | . . . . . . . 8 | |
14 | 13, 6 | wel 1466 | . . . . . . 7 |
15 | 14, 13, 4 | wrex 2394 | . . . . . 6 |
16 | 12, 15 | wa 103 | . . . . 5 |
17 | 9, 16 | wa 103 | . . . 4 |
18 | 10 | cv 1315 | . . . . . . . . . . 11 |
19 | 13 | cv 1315 | . . . . . . . . . . 11 |
20 | cltq 7061 | . . . . . . . . . . 11 | |
21 | 18, 19, 20 | wbr 3899 | . . . . . . . . . 10 |
22 | 13, 2 | wel 1466 | . . . . . . . . . 10 |
23 | 21, 22 | wa 103 | . . . . . . . . 9 |
24 | 23, 13, 4 | wrex 2394 | . . . . . . . 8 |
25 | 11, 24 | wb 104 | . . . . . . 7 |
26 | 25, 10, 4 | wral 2393 | . . . . . 6 |
27 | 10, 6 | wel 1466 | . . . . . . . . . 10 |
28 | 21, 27 | wa 103 | . . . . . . . . 9 |
29 | 28, 10, 4 | wrex 2394 | . . . . . . . 8 |
30 | 14, 29 | wb 104 | . . . . . . 7 |
31 | 30, 13, 4 | wral 2393 | . . . . . 6 |
32 | 26, 31 | wa 103 | . . . . 5 |
33 | 11, 27 | wa 103 | . . . . . . 7 |
34 | 33 | wn 3 | . . . . . 6 |
35 | 34, 10, 4 | wral 2393 | . . . . 5 |
36 | 11, 14 | wo 682 | . . . . . . . 8 |
37 | 21, 36 | wi 4 | . . . . . . 7 |
38 | 37, 13, 4 | wral 2393 | . . . . . 6 |
39 | 38, 10, 4 | wral 2393 | . . . . 5 |
40 | 32, 35, 39 | w3a 947 | . . . 4 |
41 | 17, 40 | wa 103 | . . 3 |
42 | 41, 2, 6 | copab 3958 | . 2 |
43 | 1, 42 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: npsspw 7247 elinp 7250 |
Copyright terms: Public domain | W3C validator |