-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_258.txt
77 lines (71 loc) · 1.29 KB
/
pm_258.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
# PM Chapter 258 proof relations
volume 3
part 5
section D
page 97
Thm 258.1
<- 250.101 2.03 10.1 40.13 []<->
page 98
Thm 258.101
<- 250.101 2.03 10.1 40.13 []<->
# new tactic []=
Thm 258.11
<- 40.53 40.151 10.29 40.1 22.42 22.46 258.101
# new tactic []=
Thm 258.111
<- 40.53 40.151 10.29 40.1 22.42 22.46 258.101
Thm 258.12
<- 258.1 258.101 258.11 258.111
Thm 258.13
<- 258.1 2.03 258.11 []->
Thm 258.131
<- 258.1 2.03 258.11 []->
Thm 258.14
<- 258.12 258.13 258.131
Thm 258.2
<- 258.14 257.34
Thm 258.201
<- 258.14 257.34
Thm 258.202
Thm 258.203
Thm 258.21
<- 258.13 258.2 40.151 258.1 []->
Thm 258.211
page 99
Thm 258.22
<- 258.21 257.13 210.233 []->
Thm 258.221
Thm 258.23
<- 258.2 258.22 250.23 205.121
Thm 258.231
Thm 258.24
<- 258.1 258.13 257.1 257.123 258.22 257.12
Thm 258.241
Thm 258.242
Thm 258.243
Thm 258.3
<- 80.14 258.101 257.35 257.14 []->
page 100
Thm 258.301
<- 257.36 258.241 40.1 258.101 257.121 []->
Thm 258.31
<- 80.14 150.36 257.14 150.22 202.54 257.125 83.21 258.241 258.301 257.36 []->
Thm 258.32
<- 258.3 258.31
Thm 258.321
<- 250.242 257.35 []->
Thm 258.33
<- 80.14 258.321 150.4 205.1 258.3 []->
page 101
Thm 258.34
<- 250.5 258.33
Thm 258.35
<- 200.12 250.51 258.32
Thm 258.36
<- 258.35 60.37 83.901
Thm 258.37
<- 258.36 88.33
Thm 258.38
<- 255.73 258.37 117.54 117.55
Thm 258.39
<- 258.38