df-inp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > df-inp		Unicode version

Definition df-inp 7641

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.)

**Assertion**
Ref	Expression
df-inp	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Distinct variable group:

**Detailed syntax breakdown of Definition df-inp**
Step	Hyp	Ref	Expression
1		cnp 7466	. 2
2		vl	. . . . . . . 8
3	2	cv 1394	. . . . . . 7
4		cnq 7455	. . . . . . 7
5	3, 4	wss 3197	. . . . . 6
6		vu	. . . . . . . 8
7	6	cv 1394	. . . . . . 7
8	7, 4	wss 3197	. . . . . 6
9	5, 8	wa 104	. . . . 5 $/\$
10		vq	. . . . . . . 8
11	10, 2	wel 2201	. . . . . . 7
12	11, 10, 4	wrex 2509	. . . . . 6
13		vr	. . . . . . . 8
14	13, 6	wel 2201	. . . . . . 7
15	14, 13, 4	wrex 2509	. . . . . 6
16	12, 15	wa 104	. . . . 5 $/\$
17	9, 16	wa 104	. . . 4 $/\$ $/\$ $/\$
18	10	cv 1394	. . . . . . . . . . 11
19	13	cv 1394	. . . . . . . . . . 11
20		cltq 7460	. . . . . . . . . . 11
21	18, 19, 20	wbr 4082	. . . . . . . . . 10
22	13, 2	wel 2201	. . . . . . . . . 10
23	21, 22	wa 104	. . . . . . . . 9 $/\$
24	23, 13, 4	wrex 2509	. . . . . . . 8 $/\$
25	11, 24	wb 105	. . . . . . 7 $/\$
26	25, 10, 4	wral 2508	. . . . . 6 $/\$
27	10, 6	wel 2201	. . . . . . . . . 10
28	21, 27	wa 104	. . . . . . . . 9 $/\$
29	28, 10, 4	wrex 2509	. . . . . . . 8 $/\$
30	14, 29	wb 105	. . . . . . 7 $/\$
31	30, 13, 4	wral 2508	. . . . . 6 $/\$
32	26, 31	wa 104	. . . . 5 $/\$ $/\$ $/\$
33	11, 27	wa 104	. . . . . . 7 $/\$
34	33	wn 3	. . . . . 6 $/\$
35	34, 10, 4	wral 2508	. . . . 5 $/\$
36	11, 14	wo 713	. . . . . . . 8 $\/$
37	21, 36	wi 4	. . . . . . 7 $\/$
38	37, 13, 4	wral 2508	. . . . . 6 $\/$
39	38, 10, 4	wral 2508	. . . . 5 $\/$
40	32, 35, 39	w3a 1002	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
41	17, 40	wa 104	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
42	41, 2, 6	copab 4143	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
43	1, 42	wceq 1395	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff set class

This definition is referenced by: npsspw 7646 elinp 7649

W3C validator