OAI/Analysis/Naimark/Recursion.lean

GitHub source file

207 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.NaimarkZFC.ChronologicalHistory line 14
2. structure OAI.NaimarkZFC.ChronologicalData line 37
3. def OAI.NaimarkZFC.TracialStage.dummyPair line 43
4. lemma OAI.NaimarkZFC.TracialStage.dummyPair_trace line 50
5. lemma OAI.NaimarkZFC.TracialStage.dummyPair_leftPeak line 51
6. lemma OAI.NaimarkZFC.TracialStage.base_isClosed line 52
7. lemma OAI.NaimarkZFC.TracialStage.generatedFamily_zero line 55
8. lemma OAI.NaimarkZFC.TracialStage.base_simple line 64
9. lemma OAI.NaimarkZFC.TracialStage.base_separable line 76
10. abbrev OAI.NaimarkZFC.ChronologicalData.algebra line 84
11. lemma OAI.NaimarkZFC.ChronologicalData.pureUEP line 86
12. lemma OAI.NaimarkZFC.ChronologicalData.countable_determination line 93
13. lemma OAI.NaimarkZFC.ChronologicalData.state_count line 105
14. structure OAI.NaimarkZFC.ChronologicalStage line 120
15. structure OAI.NaimarkZFC.ChronologicalStage.Hom line 127
16. def OAI.NaimarkZFC.ChronologicalStage.Hom.id line 140
17. def OAI.NaimarkZFC.ChronologicalStage.Hom.comp line 148
18. lemma OAI.NaimarkZFC.ChronologicalStage.Hom.comp_embedding line 160
19. instance OAI.NaimarkZFC.ChronologicalStage.(instance at line 164) line 164
20. def OAI.NaimarkZFC.ChronologicalStage.forget line 172
21. def OAI.NaimarkZFC.ChronologicalStage.initialHistory line 178
22. def OAI.NaimarkZFC.ChronologicalStage.initial line 200
23. lemma OAI.NaimarkZFC.PeakingPairData.hnnAmbient_of_data line 214
24. lemma OAI.NaimarkZFC.PeakingPairData.exists_reparam_pair line 228
25. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.transport line 237
26. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.same_data line 266
27. lemma OAI.NaimarkZFC.generatedFamily_congr_on line 281
28. lemma OAI.NaimarkZFC.closed_map_isClosed line 287
29. def OAI.NaimarkZFC.closedMapEquiv line 292
30. lemma OAI.NaimarkZFC.closedMapEquiv_apply line 300
31. lemma OAI.NaimarkZFC.PeakingPairData.states_restrict_of_peaks line 314
32. lemma OAI.NaimarkZFC.PeakingPairData.mapped_presentation_data line 322
33. lemma OAI.NaimarkZFC.PeakingPairData.exists_mapped_peaking_data line 355
34. lemma OAI.NaimarkZFC.PeakingPairData.mapped_ambient_from_data line 378
35. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.map line 399
36. lemma OAI.NaimarkZFC.PeakingPairData.PairDistinctOn.map line 419
37. def OAI.NaimarkZFC.TracialStage.Hom.pushPair line 450
38. lemma OAI.NaimarkZFC.TracialStage.Hom.pushPair_peak line 455
39. lemma OAI.NaimarkZFC.TracialStage.Hom.pushPair_trace line 457
40. lemma OAI.NaimarkZFC.TracialStage.Hom.image_base line 460
41. lemma OAI.NaimarkZFC.TracialStage.Hom.generatedFamily_map line 466
42. lemma OAI.NaimarkZFC.TracialStage.Hom.mapped_mem line 471
43. lemma OAI.NaimarkZFC.ChronologicalHistory.mapped_presentation line 482
44. lemma OAI.NaimarkZFC.ChronologicalHistory.mapped_inequivalent line 500
45. def OAI.NaimarkZFC.ChronologicalHistory.push line 512
46. lemma OAI.NaimarkZFC.ChronologicalStage.Hom.algebra_map line 535
47. lemma OAI.NaimarkZFC.ChronologicalData.image_generated_range line 551
48. lemma OAI.NaimarkZFC.ChronologicalData.image_mem line 559
49. lemma OAI.NaimarkZFC.ChronologicalData.updated_generated line 564
50. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.same_data line 602
51. lemma OAI.NaimarkZFC.PeakingPairData.PairDistinctOn.same_peaks line 610
52. lemma OAI.NaimarkZFC.generatedFamily_update_before line 628
53. lemma OAI.NaimarkZFC.ChronologicalHistory.inserted_peak_mem line 643
54. def OAI.NaimarkZFC.ChronologicalHistory.insertActive line 653
55. def OAI.NaimarkZFC.fullImageEquiv line 735
56. lemma OAI.NaimarkZFC.fullImageEquiv_apply line 744
57. def OAI.NaimarkZFC.fullTopEquiv line 748
58. lemma OAI.NaimarkZFC.fullTopEquiv_apply line 752
59. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.fullImage line 759
60. lemma OAI.NaimarkZFC.PeakingPairData.PairDistinctOn.fullImage line 770
61. lemma OAI.NaimarkZFC.PeakingPairData.hnnLetter_starPair line 796
62. lemma OAI.NaimarkZFC.PeakingPairData.hnn_generated_starPair line 803
63. lemma OAI.NaimarkZFC.PeakingPairData.hnn_ambient_literal line 809
64. abbrev OAI.NaimarkZFC.ChronologicalStage.hnnEmbedding line 835
65. abbrev OAI.NaimarkZFC.ChronologicalStage.hnnPriorHistory line 836
66. abbrev OAI.NaimarkZFC.ChronologicalStage.hnnNewPair line 837
67. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_new_left line 840
68. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_new_supported line 846
69. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_before_range line 851
70. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_after_generated line 855
71. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_new_presentation line 860
72. lemma OAI.NaimarkZFC.ChronologicalStage.hnn_new_inequivalent line 876
73. def OAI.NaimarkZFC.ChronologicalStage.hnnHistory line 885
74. abbrev OAI.NaimarkZFC.ChronologicalStage.hnnSuccessor line 892
75. def OAI.NaimarkZFC.ChronologicalStage.hnnHom line 895
76. def OAI.NaimarkZFC.ChronologicalData.advanceInactive line 920
77. def OAI.NaimarkZFC.ChronologicalStage.inactiveSuccessor line 950
78. def OAI.NaimarkZFC.ChronologicalStage.inactiveHom line 953
79. def OAI.NaimarkZFC.KOS.SimpleSeparableRows line 970
80. def OAI.NaimarkZFC.ChronologicalStage.coreBase line 979
81. lemma OAI.NaimarkZFC.ChronologicalStage.exists_supported_pair line 982
82. theorem OAI.NaimarkZFC.ChronologicalStage.exists_joining_successor line 1003
83. def OAI.NaimarkZFC.TracialStage.bond line 1030
84. instance OAI.NaimarkZFC.TracialStage.bond_directed line 1033
85. instance OAI.NaimarkZFC.TracialStage.bond_isometric line 1044
86. abbrev OAI.NaimarkZFC.TracialStage.LimitCarrier line 1048
87. def OAI.NaimarkZFC.TracialStage.limitIncl line 1050
88. lemma OAI.NaimarkZFC.TracialStage.limitIncl_injective line 1053
89. lemma OAI.NaimarkZFC.TracialStage.limitIncl_compatible line 1056
90. lemma OAI.NaimarkZFC.TracialStage.limitIncl_base_eq line 1060
91. def OAI.NaimarkZFC.TracialStage.limitTrace line 1066
92. lemma OAI.NaimarkZFC.TracialStage.limitTrace_state line 1070
93. lemma OAI.NaimarkZFC.TracialStage.limitTrace_tracial line 1073
94. lemma OAI.NaimarkZFC.TracialStage.limitTrace_stage line 1077
95. lemma OAI.NaimarkZFC.TracialStage.limitIncl_uep line 1083
96. def OAI.NaimarkZFC.TracialStage.directLimit line 1086
97. def OAI.NaimarkZFC.TracialStage.directLimitHom line 1099
98. lemma OAI.NaimarkZFC.TracialStage.directLimitHom_compatible line 1106
99. lemma OAI.NaimarkZFC.TracialStage.directLimitHom_dense line 1111
100. def OAI.NaimarkZFC.ChronologicalStage.limitStage line 1123
101. def OAI.NaimarkZFC.ChronologicalStage.limitEmbedding line 1124
102. def OAI.NaimarkZFC.ChronologicalStage.limitHeight line 1127
103. lemma OAI.NaimarkZFC.ChronologicalStage.height_le_limit line 1129
104. def OAI.NaimarkZFC.ChronologicalStage.limitIndex line 1132
105. lemma OAI.NaimarkZFC.ChronologicalStage.limitIndex_spec line 1135
106. lemma OAI.NaimarkZFC.ChronologicalStage.limit_embedding_compatible line 1139
107. lemma OAI.NaimarkZFC.ChronologicalStage.limit_generator_agree line 1144
108. lemma OAI.NaimarkZFC.ChronologicalStage.limit_peak_agree line 1152
109. lemma OAI.NaimarkZFC.ChronologicalStage.limit_active_agree line 1161
110. lemma OAI.NaimarkZFC.ChronologicalStage.limit_dependency_agree line 1168
111. def OAI.NaimarkZFC.ChronologicalStage.limitGenerator line 1175
112. def OAI.NaimarkZFC.ChronologicalStage.limitActive line 1180
113. def OAI.NaimarkZFC.ChronologicalStage.limitDependency line 1183
114. def OAI.NaimarkZFC.ChronologicalStage.limitPair line 1186
115. lemma OAI.NaimarkZFC.ChronologicalStage.limitGenerator_stage line 1193
116. lemma OAI.NaimarkZFC.ChronologicalStage.limitActive_stage line 1199
117. lemma OAI.NaimarkZFC.ChronologicalStage.limitDependency_stage line 1208
118. lemma OAI.NaimarkZFC.ChronologicalStage.limitPair_peak_stage line 1214
119. lemma OAI.NaimarkZFC.ChronologicalStage.limitPair_trace line 1221
120. lemma OAI.NaimarkZFC.ChronologicalStage.limitPair_leftPeak line 1226
121. lemma OAI.NaimarkZFC.ChronologicalStage.limit_algebra_map line 1234
122. lemma OAI.NaimarkZFC.ChronologicalStage.limit_generated_eq line 1249
123. lemma OAI.NaimarkZFC.ChronologicalStage.limit_peak_mem line 1255
124. lemma OAI.NaimarkZFC.ChronologicalStage.limit_supported line 1264
125. lemma OAI.NaimarkZFC.ChronologicalStage.limit_chronological line 1275
126. lemma OAI.NaimarkZFC.ChronologicalStage.limit_inequivalent line 1300
127. lemma OAI.NaimarkZFC.ChronologicalStage.limit_inactive line 1319
128. lemma OAI.NaimarkZFC.ChronologicalStage.limit_generated line 1327
129. def OAI.NaimarkZFC.ChronologicalStage.limitHistory line 1345
130. def OAI.NaimarkZFC.ChronologicalStage.directLimit line 1366
131. def OAI.NaimarkZFC.ChronologicalStage.directLimitHom line 1367
132. def OAI.NaimarkZFC.ChronologicalStage.directLimitCocone line 1375
133. lemma OAI.NaimarkZFC.ChronologicalStage.prefix_congr_obj line 1395
134. lemma OAI.NaimarkZFC.ChronologicalStage.prefix_congr_arrow line 1403
135. lemma OAI.NaimarkZFC.ChronologicalStage.prefix_congr_map line 1410
136. def OAI.NaimarkZFC.ChronologicalStage.prefixMap line 1418
137. lemma OAI.NaimarkZFC.ChronologicalStage.prefixMap_refl line 1422
138. lemma OAI.NaimarkZFC.ChronologicalStage.prefixMap_comp line 1425
139. def OAI.NaimarkZFC.ChronologicalStage.gluePrefixes line 1430
140. lemma OAI.NaimarkZFC.ChronologicalStage.gluePrefixes_arrow line 1436
141. lemma OAI.NaimarkZFC.ChronologicalStage.restrictionLE_of_glued_cocone line 1443
142. def OAI.NaimarkZFC.ChronologicalStage.prefixSystem line 1468
143. lemma OAI.NaimarkZFC.ChronologicalStage.restriction_extendToSucc line 1487
144. abbrev OAI.NaimarkZFC.ChronologicalStage.SuccessorRule line 1497
145. lemma OAI.NaimarkZFC.ChronologicalStage.section_coherent line 1503
146. def OAI.NaimarkZFC.ChronologicalStage.recursionData line 1509
147. def OAI.NaimarkZFC.ChronologicalStage.recursivePrefixes line 1524
148. lemma OAI.NaimarkZFC.ChronologicalStage.recursivePrefixes_compatible line 1527
149. def OAI.NaimarkZFC.ChronologicalStage.recursiveTower line 1532
150. lemma OAI.NaimarkZFC.ChronologicalStage.recursivePrefixes_bot line 1537
151. lemma OAI.NaimarkZFC.ChronologicalStage.recursivePrefixes_succ line 1542
152. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_obj line 1561
153. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_arrow line 1564
154. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_bot line 1570
155. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_succ_arrow line 1574
156. def OAI.NaimarkZFC.ChronologicalStage.earlierPrefixes line 1589
157. lemma OAI.NaimarkZFC.ChronologicalStage.recursivePrefixes_limit line 1594
158. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_limit_height line 1610
159. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_succ_height line 1621
160. theorem OAI.NaimarkZFC.ChronologicalStage.recursiveTower_height_le line 1630
161. def OAI.NaimarkZFC.TracialStage.Hom.pureLift line 1656
162. lemma OAI.NaimarkZFC.TracialStage.Hom.pureLift_pure line 1658
163. lemma OAI.NaimarkZFC.TracialStage.Hom.pureLift_restrict line 1660
164. def OAI.NaimarkZFC.ChronologicalStage.pureList line 1667
165. lemma OAI.NaimarkZFC.ChronologicalStage.pureList_pure line 1672
166. lemma OAI.NaimarkZFC.ChronologicalStage.pureList_covers line 1679
167. def OAI.NaimarkZFC.ChronologicalStage.joiningChoice line 1689
168. lemma OAI.NaimarkZFC.ChronologicalStage.joiningChoice_height line 1694
169. lemma OAI.NaimarkZFC.ChronologicalStage.joiningChoice_treated line 1698
170. def OAI.NaimarkZFC.ChronologicalStage.scheduledTarget line 1709
171. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledTarget_pure line 1718
172. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledTarget_restrict line 1725
173. def OAI.NaimarkZFC.ChronologicalStage.scheduledRule line 1740
174. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledRule_height line 1745
175. lemma OAI.NaimarkZFC.ChronologicalStage.arrowMap_extendToSucc_through line 1758
176. def OAI.NaimarkZFC.ChronologicalStage.Treated line 1782
177. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledRule_treated line 1791
178. lemma OAI.NaimarkZFC.ChronologicalStage.recursiveTower_through_succ_arrow line 1809
179. theorem OAI.NaimarkZFC.ChronologicalStage.recursiveTower_treated line 1818
180. abbrev OAI.NaimarkZFC.ConstructionIndex line 1829
181. lemma OAI.NaimarkZFC.construction_ordinal_limit line 1831
182. instance OAI.NaimarkZFC.constructionIndex_nonempty line 1834
183. instance OAI.NaimarkZFC.constructionIndex_orderBot line 1837
184. instance OAI.NaimarkZFC.constructionIndex_noMax line 1840
185. lemma OAI.NaimarkZFC.constructionIndex_bot line 1847
186. lemma OAI.NaimarkZFC.constructionIndex_monotone line 1854
187. lemma OAI.NaimarkZFC.constructionIndex_succ_bound line 1857
188. lemma OAI.NaimarkZFC.constructionIndex_cardinal line 1862
189. lemma OAI.NaimarkZFC.ChronologicalStage.limit_countable_support_bounded line 1872
190. lemma OAI.NaimarkZFC.ChronologicalStage.limit_support_le_range line 1885
191. theorem OAI.NaimarkZFC.ChronologicalStage.limit_eventual_pure line 1893
192. abbrev OAI.NaimarkZFC.ChronologicalStage.FullRule line 1916
193. abbrev OAI.NaimarkZFC.ChronologicalStage.fullTower line 1921
194. lemma OAI.NaimarkZFC.ChronologicalStage.fullTower_height line 1929
195. lemma OAI.NaimarkZFC.ChronologicalStage.fullTower_count line 1935
196. theorem OAI.NaimarkZFC.ChronologicalStage.fullTower_pure_reference line 1939
197. instance OAI.NaimarkZFC.liftStarRing line 1980
198. instance OAI.NaimarkZFC.liftStarModule line 1986
199. instance OAI.NaimarkZFC.liftCStarRing line 1989
200. instance OAI.NaimarkZFC.liftCStarAlgebra line 1994
201. def OAI.NaimarkZFC.liftStarAlgEquiv line 1996
202. lemma OAI.NaimarkZFC.liftStarAlgEquiv_apply line 2006
203. theorem OAI.NaimarkZFC.rankOne_isCompact line 2013
204. theorem OAI.NaimarkZFC.compacts_representation_map_one line 2020
205. theorem OAI.NaimarkZFC.not_isIsomorphicToCompacts line 2037
206. lemma OAI.NaimarkZFC.pureHomogeneity_of_equiv line 2055
207. theorem OAI.NaimarkZFC.main_of_approxNearCentralRows line 2067