OAI/Dynamics/MultipleMixing/ExactLines.lean

GitHub source file

314 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Rokhlin.closure_image_dense_span line 15
2. lemma OAI.Rokhlin.pullback_dense_span line 43
3. lemma OAI.Rokhlin.torusWord_pullback_dense line 54
4. lemma OAI.Rokhlin.JoiningOperator.torusWord_contraction line 76
5. lemma OAI.Rokhlin.JoiningOperator.ratio_field_le_active line 132
6. lemma OAI.Rokhlin.ConditionalFibres.ae_kernel_joint line 151
7. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_torus_completeness line 171
8. lemma OAI.Rokhlin.field_finset_observation line 276
9. lemma OAI.Rokhlin.field_pair_finset_union line 282
10. lemma OAI.Rokhlin.field_finset_grid line 290
11. lemma OAI.Rokhlin.field_grid_pair_inner_union line 297
12. structure OAI.Rokhlin.ComplementSplit line 311
13. abbrev OAI.Rokhlin.ComplementSplit.partition line 324
14. instance OAI.Rokhlin.ComplementSplit.(instance at line 327) line 327
15. lemma OAI.Rokhlin.ComplementSplit.union_eq line 332
16. def OAI.Rokhlin.ComplementSplit.singleton line 345
17. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_pair_preserving line 371
18. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_complement_invariant line 381
19. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_complement_invariant line 404
20. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive_complement_invariant line 428
21. lemma OAI.Rokhlin.ternary_unit_const_of_nonzero_mean line 446
22. lemma OAI.Rokhlin.ternary_line_dichotomy line 490
23. def OAI.Rokhlin.JoiningOperator.splitExact line 524
24. lemma OAI.Rokhlin.JoiningOperator.zero_mem_splitExact line 528
25. lemma OAI.Rokhlin.JoiningOperator.smul_mem_splitExact line 532
26. lemma OAI.Rokhlin.JoiningOperator.circle_mem_splitExact line 537
27. lemma OAI.Rokhlin.JoiningOperator.circleLp_dichotomy line 545
28. lemma OAI.Rokhlin.JoiningOperator.splitExact_dichotomy line 574
29. lemma OAI.Rokhlin.JoiningOperator.circleLp_contraction line 592
30. lemma OAI.Rokhlin.JoiningOperator.splitExact_le_active line 617
31. lemma OAI.Rokhlin.torus_circle_pull line 634
32. lemma OAI.Rokhlin.torus_circle_dense line 645
33. lemma OAI.Rokhlin.JoiningOperator.torus_exact_split line 662
34. lemma OAI.Rokhlin.JoiningOperator.torus_split_inter_span line 674
35. lemma OAI.Rokhlin.nonzero_inner_in_closedSpan line 698
36. theorem OAI.Rokhlin.common_exact_all_splits line 714
37. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowSplitExact line 758
38. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnSplitExact line 761
39. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_exact_split_span line 765
40. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowSplitExact_dichotomy line 795
41. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnSplitExact_dichotomy line 809
42. def OAI.Rokhlin.ArrayObjects.Object.Rolled.allSplitExact line 823
43. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.allSplitExact_span line 827
44. def OAI.Rokhlin.ArrayObjects.Object.Rolled.oneColumn line 846
45. def OAI.Rokhlin.ArrayObjects.Object.Rolled.oneRow line 849
46. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_oneColumn line 853
47. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_oneRow line 856
48. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnCellLaw line 859
49. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowCellLaw line 861
50. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 864) line 864
51. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 866) line 866
52. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.proper_columns_product line 870
53. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.proper_rows_product line 887
54. lemma OAI.Rokhlin.ComplementSplit.two_le_card_compl line 905
55. lemma OAI.Rokhlin.ComplementSplit.rest_nonempty line 911
56. abbrev OAI.Rokhlin.ComplementSplit.singletonFor line 917
57. def OAI.Rokhlin.ComplementSplit.restIndex line 920
58. def OAI.Rokhlin.hybrid line 935
59. lemma OAI.Rokhlin.measurePreserving_hybrid line 938
60. lemma OAI.Rokhlin.ae_eq_const_of_omit line 948
61. lemma OAI.Rokhlin.pure_product_of_singleton_splits line 973
62. lemma OAI.Rokhlin.circle_split_witness line 1009
63. lemma OAI.Rokhlin.full_product_of_exact_splits line 1033
64. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.complement_proper line 1068
65. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.row_all_splits_product line 1074
66. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.column_all_splits_product line 1109
67. def OAI.Rokhlin.ArrayObjects.Object.Rolled.fullExact line 1150
68. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.zero_mem_fullExact line 1160
69. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.allSplitExact_subset_fullExact line 1165
70. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive_le_fullExact_span line 1187
71. theorem OAI.Rokhlin.ae_map_descent line 1202
72. lemma OAI.Rokhlin.random_projection_exactness line 1236
73. lemma OAI.Rokhlin.essential_projection_not_ae_zero line 1265
74. lemma OAI.Rokhlin.active_projection_not_ae_zero line 1275
75. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.Cell line 1291
76. def OAI.Rokhlin.ArrayObjects.Object.Rolled.padCell line 1293
77. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_padCell line 1295
78. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotCell line 1298
79. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_slotCell line 1300
80. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotRest line 1304
81. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_slotRest line 1306
82. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotLocal line 1309
83. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 1310) line 1310
84. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotActive line 1312
85. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotActive_eq line 1319
86. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotActive_closed line 1325
87. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 1332) line 1332
88. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_single_row line 1336
89. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_single_column line 1345
90. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotCell_marginal line 1355
91. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.row_marginal_fibre line 1364
92. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.column_marginal_fibre line 1379
93. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.singleton_cellLaw line 1385
94. lemma OAI.Rokhlin.iIndepFun_map_iff_measurable line 1406
95. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotTuple line 1422
96. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_slotTuple line 1425
97. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotTupleKernel line 1428
98. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 1430) line 1430
99. def OAI.Rokhlin.ArrayObjects.Object.Rolled.tupleParameter line 1433
100. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_tupleParameter line 1435
101. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotTuple_marginal line 1439
102. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.tuple_planes_product line 1455
103. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotTuple_proper line 1467
104. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_good_tuple_set line 1485
105. def OAI.Rokhlin.productTupleKernel line 1513
106. instance OAI.Rokhlin.(instance at line 1515) line 1515
107. lemma OAI.Rokhlin.exists_good_tuple_kernel line 1518
108. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTuple line 1560
109. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawTuple line 1562
110. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTupleKernel line 1565
111. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 1566) line 1566
112. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTuple_marginal line 1569
113. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTuple_proper line 1581
114. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_good_tuple_kernel line 1598
115. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTuple_time_commute line 1613
116. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTuple_time_preserving line 1616
117. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.tupleParameter_time line 1628
118. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.goodTuple_time_preserving line 1631
119. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exactCode_time line 1641
120. def OAI.Rokhlin.exactCodeEquivTransport line 1669
121. def OAI.Rokhlin.measurableCircleSubgroup line 1711
122. abbrev OAI.Rokhlin.MeasurableCircle line 1716
123. instance OAI.Rokhlin.measurableCircleCoeFun line 1717
124. lemma OAI.Rokhlin.measurableCircle_measurable line 1718
125. def OAI.Rokhlin.phaseSubgroup line 1721
126. abbrev OAI.Rokhlin.ProjectiveCircle line 1734
127. def OAI.Rokhlin.projectiveCircle line 1736
128. lemma OAI.Rokhlin.projectiveCircle_eq_iff line 1739
129. lemma OAI.Rokhlin.projectiveCircle_mul line 1758
130. lemma OAI.Rokhlin.projectiveCircle_one line 1762
131. lemma OAI.Rokhlin.projectiveCircle_inv line 1763
132. def OAI.Rokhlin.exactCircleTuples line 1773
133. def OAI.Rokhlin.tupleProjectivize line 1789
134. def OAI.Rokhlin.exactProjectiveTuples line 1795
135. def OAI.Rokhlin.exactProjectiveSlot line 1799
136. lemma OAI.Rokhlin.exactCircleTuples_constant_of_slot line 1806
137. lemma OAI.Rokhlin.exactProjectiveSlot_injective line 1851
138. def OAI.Rokhlin.exactProjectiveMatching line 1871
139. def OAI.Rokhlin.HilbertCode.projective line 1891
140. lemma OAI.Rokhlin.HilbertCode.projective_injective line 1894
141. lemma OAI.Rokhlin.HilbertCode.projective_encode_phase line 1911
142. lemma OAI.Rokhlin.exact_code_projective_mem line 1934
143. lemma OAI.Rokhlin.exact_projective_has_codes line 1944
144. lemma OAI.Rokhlin.HilbertCode.distance_self line 1970
145. lemma OAI.Rokhlin.exactCode_unique_slot line 1974
146. lemma OAI.Rokhlin.exactCode_slot_embedding line 1989
147. def OAI.Rokhlin.exactMatching line 2004
148. lemma OAI.Rokhlin.measurable_exactMatching line 2008
149. lemma OAI.Rokhlin.exactMatching_exact line 2019
150. abbrev OAI.Rokhlin.ExactCodeSlot line 2036
151. lemma OAI.Rokhlin.codeSlot_projective_range line 2040
152. lemma OAI.Rokhlin.codeSlot_projective_injective line 2057
153. def OAI.Rokhlin.codeSlotEquivProjective line 2068
154. def OAI.Rokhlin.codeSlotMatching line 2085
155. lemma OAI.Rokhlin.exactSlot_transport line 2102
156. def OAI.Rokhlin.localGraphTimeEquiv line 2114
157. lemma OAI.Rokhlin.rectangle_first_commutes line 2167
158. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_active_commutes_corner line 2192
159. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_active_commutes line 2233
160. lemma OAI.Rokhlin.orthogonal_line_projection line 2247
161. lemma OAI.Rokhlin.inf_projection_on_left line 2267
162. lemma OAI.Rokhlin.common_lines_projection line 2280
163. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_row_line_projection line 2308
164. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_full_row_column_exact line 2331
165. lemma OAI.Rokhlin.lp_star_zero line 2373
166. lemma OAI.Rokhlin.lp_star_sub line 2379
167. lemma OAI.Rokhlin.lp_star_smul line 2386
168. lemma OAI.Rokhlin.lp_inner_star_star line 2392
169. lemma OAI.Rokhlin.lp_inner_star_right line 2403
170. lemma OAI.Rokhlin.lp_star_projection line 2407
171. lemma OAI.Rokhlin.JoiningOperator.operator_star line 2427
172. lemma OAI.Rokhlin.JoiningOperator.family_star line 2441
173. lemma OAI.Rokhlin.JoiningOperator.family_adjoint_star line 2449
174. lemma OAI.Rokhlin.JoiningOperator.family_active_star line 2459
175. lemma OAI.Rokhlin.JoiningOperator.family_active_projection_star line 2471
176. lemma OAI.Rokhlin.JoiningOperator.operator_circle_exact line 2478
177. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_star line 2507
178. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_star line 2514
179. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive_star line 2521
180. lemma OAI.Rokhlin.conditional_ae_descent line 2533
181. lemma OAI.Rokhlin.JoiningOperator.family_circle_exact line 2552
182. lemma OAI.Rokhlin.binary_projection_transfer line 2570
183. lemma OAI.Rokhlin.circleLp_inv line 2596
184. abbrev OAI.Rokhlin.TriplePartition.split line 2609
185. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowSplitExact_le_rowActive line 2619
186. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_row_membership_transfer line 2631
187. lemma OAI.Rokhlin.JoiningOperator.measurePreserving_of_comp line 2701
188. lemma OAI.Rokhlin.JoiningOperator.active_pullback line 2707
189. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_field line 2723
190. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.row_rest_field line 2728
191. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.column_rest_field line 2743
192. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_single_slot line 2759
193. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_single_slot line 2785
194. def OAI.Rokhlin.JoiningOperator.pullEquiv line 2820
195. lemma OAI.Rokhlin.JoiningOperator.pullEquiv_coe line 2834
196. lemma OAI.Rokhlin.JoiningOperator.operator_reparam line 2837
197. lemma OAI.Rokhlin.JoiningOperator.active_reparam line 2854
198. lemma OAI.Rokhlin.circleLp_pull line 2881
199. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.CellAt line 2894
200. def OAI.Rokhlin.ArrayObjects.Object.Rolled.collapseCell line 2896
201. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.collapse_cell_row line 2909
202. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.collapse_cell_column line 2912
203. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotActive line 2915
204. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotActive_eq line 2921
205. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotActive_closed line 2926
206. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 2932) line 2932
207. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.row_rest_field_mixed line 2935
208. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.column_rest_field_mixed line 2949
209. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.singleton_collapse_preserving line 2964
210. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_mixed_slot line 2981
211. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_mixed_slot line 3006
212. lemma OAI.Rokhlin.singleton_proper line 3046
213. lemma OAI.Rokhlin.pair_complement_nonempty line 3051
214. def OAI.Rokhlin.singletonSplit line 3060
215. abbrev OAI.Rokhlin.pairPartition line 3071
216. lemma OAI.Rokhlin.pairPartition_P line 3076
217. lemma OAI.Rokhlin.pairPartition_A line 3078
218. lemma OAI.Rokhlin.pairPartition_B line 3080
219. def OAI.Rokhlin.circleComplete line 3091
220. lemma OAI.Rokhlin.circleComplete_self line 3095
221. lemma OAI.Rokhlin.measurable_circleComplete line 3098
222. lemma OAI.Rokhlin.prod_complement line 3106
223. lemma OAI.Rokhlin.circleComplete_prod line 3111
224. lemma OAI.Rokhlin.prod_equation_solve line 3120
225. lemma OAI.Rokhlin.prod_pair_solve line 3130
226. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_row_membership_transfer line 3144
227. lemma OAI.Rokhlin.projection_transport line 3180
228. lemma OAI.Rokhlin.binary_projection_transport line 3193
229. lemma OAI.Rokhlin.JoiningOperator.circleLp_operator line 3210
230. lemma OAI.Rokhlin.prod_complement_split line 3231
231. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_tuple_active line 3243
232. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_tuple_rowSplitExact line 3259
233. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_row_line_projection line 3284
234. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawExactCone line 3312
235. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawExactCone_smul line 3318
236. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.oneRow_single_column line 3325
237. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fullExact_raw_column line 3332
238. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_row_active_to_column_exact line 3365
239. lemma OAI.Rokhlin.HilbertCode.encode_injective line 3398
240. def OAI.Rokhlin.exactCodeVectors line 3411
241. def OAI.Rokhlin.exactCodeSpan line 3414
242. lemma OAI.Rokhlin.exactCodeSpan_congr_kernel line 3418
243. lemma OAI.Rokhlin.exactCircle_mem_codeSpan line 3428
244. lemma OAI.Rokhlin.exactVector_circle_tuple line 3441
245. lemma OAI.Rokhlin.exactCodeSpan_sections line 3460
246. lemma OAI.Rokhlin.canonical_smul_exact_tuple line 3509
247. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph line 3548
248. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCode_of_cone line 3554
249. def OAI.Rokhlin.joiningPosterior line 3594
250. instance OAI.Rokhlin.(instance at line 3595) line 3595
251. lemma OAI.Rokhlin.joiningPosterior_conditional line 3599
252. lemma OAI.Rokhlin.posterior_memLp line 3614
253. def OAI.Rokhlin.posteriorVector line 3624
254. lemma OAI.Rokhlin.measurableSection_posteriorVector line 3628
255. lemma OAI.Rokhlin.posteriorVector_eq_operator line 3635
256. lemma OAI.Rokhlin.hilbertTestFunction_bounded line 3667
257. def OAI.Rokhlin.posteriorTest line 3687
258. lemma OAI.Rokhlin.measurableSection_posteriorTest line 3692
259. lemma OAI.Rokhlin.posteriorTest_eq_operator line 3698
260. lemma OAI.Rokhlin.operator_range_le_iff_tests line 3707
261. lemma OAI.Rokhlin.operator_range_eq_span_tests line 3724
262. lemma OAI.Rokhlin.MeasurableSection.circle line 3740
263. lemma OAI.Rokhlin.MeasurableSection.comp line 3749
264. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotTest line 3759
265. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotTestSpan line 3762
266. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurableSection_rawSlotTest line 3765
267. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotTest_eq_operator line 3768
268. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotActive_eq_testSpan line 3776
269. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurableSet_rawSlot_mem line 3793
270. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotIndicator line 3802
271. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawSlotIndicator line 3808
272. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotIndicator_eq_true_iff line 3818
273. lemma OAI.Rokhlin.independent_equal_indicators line 3833
274. lemma OAI.Rokhlin.product_equal_positive_indicators line 3862
275. lemma OAI.Rokhlin.conditional_joint_ae_lift line 3890
276. lemma OAI.Rokhlin.conditional_equal_positive_indicators line 3898
277. lemma OAI.Rokhlin.conditional_ae_lift line 3927
278. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameterCoordinate_conditional line 3945
279. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.coordinate_conditional_descent line 3952
280. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_diagonal_binary line 3959
281. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_coordinate_marginal line 3982
282. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_slot_mem_parameter_congr line 3989
283. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_diagonal_positive line 3996
284. lemma OAI.Rokhlin.FiniteKernel.map_pair line 4058
285. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_pair_geometry line 4074
286. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSlotIndicator_on_square line 4107
287. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_row_indicators_equal line 4128
288. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_row_membership_forced line 4149
289. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_cell_commute line 4184
290. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawExactCone_parameter_congr line 4193
291. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph_row_inclusion line 4200
292. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph_base line 4268
293. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph_canonical line 4276
294. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph_separated line 4283
295. lemma OAI.Rokhlin.iid_random_set_descent line 4309
296. def OAI.Rokhlin.essentialMembership line 4322
297. lemma OAI.Rokhlin.measurableSet_essentialMembership line 4325
298. lemma OAI.Rokhlin.mem_essentialMembership_iff line 4332
299. lemma OAI.Rokhlin.conditional_random_set_descent line 4337
300. lemma OAI.Rokhlin.iid_random_set_equality line 4350
301. lemma OAI.Rokhlin.separated_family_sections line 4365
302. lemma OAI.Rokhlin.measurableSet_enumerated_fibre_eq line 4407
303. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurableSet_rawLineGraph line 4470
304. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLineGraph_conditional_descent line 4474
305. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_localLineGraph line 4493
306. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localLineGraph_inclusion line 4560
307. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_commonLocalLineGraph line 4588
308. lemma OAI.Rokhlin.exactCode_of_circle_tuple line 4627
309. lemma OAI.Rokhlin.independent_circle_product_constant line 4660
310. lemma OAI.Rokhlin.circle_square_consistency line 4709
311. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.whole_rows_independent_fibre line 4747
312. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_marginals line 4765
313. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_exact_consistency line 4793
314. lemma OAI.Rokhlin.enumerate_without_repetition line 4843