OAI/AlgebraicTopology/Cubical/Singular.lean

GitHub source file

278 declarations, 0 contain sorry, 0 declared as axioms

Low-dimensional normalized cubical singular chains for the actual cellular comparison of arbitrary ordinary two-dimensional CW spaces. Neither cellular exactness nor a presentation theorem is included as an assumption.

  1. abbrev OAI.EilenbergGanea.CubicalSingular.I line 20
  2. abbrev OAI.EilenbergGanea.CubicalSingular.Cube₁ line 21
  3. abbrev OAI.EilenbergGanea.CubicalSingular.Cube₂ line 22
  4. abbrev OAI.EilenbergGanea.CubicalSingular.Cube₃ line 23
  5. abbrev OAI.EilenbergGanea.CubicalSingular.C₀ line 24
  6. abbrev OAI.EilenbergGanea.CubicalSingular.C₁ line 25
  7. abbrev OAI.EilenbergGanea.CubicalSingular.C₂ line 26
  8. abbrev OAI.EilenbergGanea.CubicalSingular.C₃ line 27
  9. def OAI.EilenbergGanea.CubicalSingular.edge₁ line 29
  10. def OAI.EilenbergGanea.CubicalSingular.edge₂ line 30
  11. def OAI.EilenbergGanea.CubicalSingular.face₁ line 31
  12. def OAI.EilenbergGanea.CubicalSingular.face₂ line 32
  13. def OAI.EilenbergGanea.CubicalSingular.face₃ line 33
  14. def OAI.EilenbergGanea.CubicalSingular.b₁ line 35
  15. def OAI.EilenbergGanea.CubicalSingular.b₂ line 37
  16. def OAI.EilenbergGanea.CubicalSingular.b₃ line 40
  17. theorem OAI.EilenbergGanea.CubicalSingular.b₁_single line 45
  18. theorem OAI.EilenbergGanea.CubicalSingular.b₂_single line 48
  19. theorem OAI.EilenbergGanea.CubicalSingular.b₃_single line 52
  20. theorem OAI.EilenbergGanea.CubicalSingular.b₁_b₂ line 58
  21. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_face₂ line 65
  22. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_face₃ line 66
  23. theorem OAI.EilenbergGanea.CubicalSingular.edge₂_face₃ line 67
  24. theorem OAI.EilenbergGanea.CubicalSingular.b₂_b₃ line 69
  25. def OAI.EilenbergGanea.CubicalSingular.constant₁ line 76
  26. def OAI.EilenbergGanea.CubicalSingular.degenerate₁ line 77
  27. def OAI.EilenbergGanea.CubicalSingular.degenerate₂ line 78
  28. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_degenerate₁ line 79
  29. theorem OAI.EilenbergGanea.CubicalSingular.edge₂_degenerate₁ line 81
  30. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_degenerate₂ line 83
  31. theorem OAI.EilenbergGanea.CubicalSingular.edge₂_degenerate₂ line 85
  32. def OAI.EilenbergGanea.CubicalSingular.D₁ line 87
  33. def OAI.EilenbergGanea.CubicalSingular.D₂ line 89
  34. abbrev OAI.EilenbergGanea.CubicalSingular.N₁ line 92
  35. abbrev OAI.EilenbergGanea.CubicalSingular.N₂ line 93
  36. theorem OAI.EilenbergGanea.CubicalSingular.D₁_le_ker line 95
  37. theorem OAI.EilenbergGanea.CubicalSingular.b₂_D₂ line 100
  38. def OAI.EilenbergGanea.CubicalSingular.d₁ line 117
  39. def OAI.EilenbergGanea.CubicalSingular.d₂ line 118
  40. def OAI.EilenbergGanea.CubicalSingular.d₃ line 119
  41. theorem OAI.EilenbergGanea.CubicalSingular.d₁_mk line 121
  42. theorem OAI.EilenbergGanea.CubicalSingular.d₂_mk line 122
  43. theorem OAI.EilenbergGanea.CubicalSingular.d₁_d₂ line 124
  44. theorem OAI.EilenbergGanea.CubicalSingular.d₂_d₃ line 128
  45. def OAI.EilenbergGanea.CubicalSingular.push₀ line 136
  46. def OAI.EilenbergGanea.CubicalSingular.push₁ line 138
  47. def OAI.EilenbergGanea.CubicalSingular.push₂ line 140
  48. def OAI.EilenbergGanea.CubicalSingular.push₃ line 142
  49. theorem OAI.EilenbergGanea.CubicalSingular.push₀_single line 145
  50. theorem OAI.EilenbergGanea.CubicalSingular.push₁_single line 147
  51. theorem OAI.EilenbergGanea.CubicalSingular.push₂_single line 149
  52. theorem OAI.EilenbergGanea.CubicalSingular.push₃_single line 151
  53. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_comp line 154
  54. theorem OAI.EilenbergGanea.CubicalSingular.edge₂_comp line 156
  55. theorem OAI.EilenbergGanea.CubicalSingular.face₁_comp line 158
  56. theorem OAI.EilenbergGanea.CubicalSingular.face₂_comp line 160
  57. theorem OAI.EilenbergGanea.CubicalSingular.face₃_comp line 162
  58. theorem OAI.EilenbergGanea.CubicalSingular.b₁_push line 165
  59. theorem OAI.EilenbergGanea.CubicalSingular.b₂_push line 170
  60. theorem OAI.EilenbergGanea.CubicalSingular.b₃_push line 175
  61. def OAI.EilenbergGanea.CubicalSingular.prism₀ line 182
  62. def OAI.EilenbergGanea.CubicalSingular.prism₁ line 183
  63. def OAI.EilenbergGanea.CubicalSingular.prism₂ line 184
  64. def OAI.EilenbergGanea.CubicalSingular.P₀ line 186
  65. def OAI.EilenbergGanea.CubicalSingular.P₁ line 188
  66. def OAI.EilenbergGanea.CubicalSingular.P₂ line 190
  67. theorem OAI.EilenbergGanea.CubicalSingular.P₀_single line 192
  68. theorem OAI.EilenbergGanea.CubicalSingular.P₁_single line 194
  69. theorem OAI.EilenbergGanea.CubicalSingular.P₂_single line 196
  70. theorem OAI.EilenbergGanea.CubicalSingular.prism₀_zero line 198
  71. theorem OAI.EilenbergGanea.CubicalSingular.prism₀_one line 199
  72. theorem OAI.EilenbergGanea.CubicalSingular.prism₁_edge₁_zero line 200
  73. theorem OAI.EilenbergGanea.CubicalSingular.prism₁_edge₁_one line 202
  74. theorem OAI.EilenbergGanea.CubicalSingular.prism₁_edge₂ line 204
  75. theorem OAI.EilenbergGanea.CubicalSingular.prism₂_face₁_zero line 205
  76. theorem OAI.EilenbergGanea.CubicalSingular.prism₂_face₁_one line 207
  77. theorem OAI.EilenbergGanea.CubicalSingular.prism₂_face₂ line 209
  78. theorem OAI.EilenbergGanea.CubicalSingular.prism₂_face₃ line 210
  79. theorem OAI.EilenbergGanea.CubicalSingular.prism_boundary₀ line 212
  80. theorem OAI.EilenbergGanea.CubicalSingular.prism_boundary₁ line 217
  81. theorem OAI.EilenbergGanea.CubicalSingular.prism_boundary₂ line 222
  82. theorem OAI.EilenbergGanea.CubicalSingular.P₁_D₁ line 227
  83. theorem OAI.EilenbergGanea.CubicalSingular.push₁_id line 238
  84. theorem OAI.EilenbergGanea.CubicalSingular.push₂_id line 242
  85. theorem OAI.EilenbergGanea.CubicalSingular.push₁_const_mem line 247
  86. theorem OAI.EilenbergGanea.CubicalSingular.push₂_const_mem line 257
  87. theorem OAI.EilenbergGanea.CubicalSingular.exact₁_of_contractible line 268
  88. theorem OAI.EilenbergGanea.CubicalSingular.exact₂_of_contractible line 283
  89. theorem OAI.EilenbergGanea.CubicalSingular.comp_constant₁ line 304
  90. theorem OAI.EilenbergGanea.CubicalSingular.comp_degenerate₁ line 306
  91. theorem OAI.EilenbergGanea.CubicalSingular.comp_degenerate₂ line 308
  92. theorem OAI.EilenbergGanea.CubicalSingular.push₁_D₁ line 311
  93. theorem OAI.EilenbergGanea.CubicalSingular.push₂_D₂ line 318
  94. def OAI.EilenbergGanea.CubicalSingular.pushN₁ line 328
  95. def OAI.EilenbergGanea.CubicalSingular.pushN₂ line 329
  96. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_mk line 330
  97. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_mk line 332
  98. theorem OAI.EilenbergGanea.CubicalSingular.d₁_push line 335
  99. theorem OAI.EilenbergGanea.CubicalSingular.d₂_push line 339
  100. theorem OAI.EilenbergGanea.CubicalSingular.d₃_push line 344
  101. theorem OAI.EilenbergGanea.CubicalSingular.push₁_comp line 348
  102. theorem OAI.EilenbergGanea.CubicalSingular.push₂_comp line 353
  103. theorem OAI.EilenbergGanea.CubicalSingular.push₃_comp line 358
  104. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_comp line 363
  105. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_comp line 368
  106. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_id line 373
  107. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_id line 377
  108. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_const line 382
  109. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_const line 395
  110. def OAI.EilenbergGanea.CubicalSingular.half line 414
  111. theorem OAI.EilenbergGanea.CubicalSingular.half_false_zero line 418
  112. theorem OAI.EilenbergGanea.CubicalSingular.half_true_one line 419
  113. theorem OAI.EilenbergGanea.CubicalSingular.half_mid line 420
  114. def OAI.EilenbergGanea.CubicalSingular.cut₁ line 422
  115. def OAI.EilenbergGanea.CubicalSingular.cut₂ line 423
  116. def OAI.EilenbergGanea.CubicalSingular.cut₃ line 425
  117. def OAI.EilenbergGanea.CubicalSingular.S₁ line 428
  118. def OAI.EilenbergGanea.CubicalSingular.S₂ line 430
  119. def OAI.EilenbergGanea.CubicalSingular.S₃ line 432
  120. theorem OAI.EilenbergGanea.CubicalSingular.S₁_single line 435
  121. theorem OAI.EilenbergGanea.CubicalSingular.S₂_single line 438
  122. theorem OAI.EilenbergGanea.CubicalSingular.S₃_single line 441
  123. theorem OAI.EilenbergGanea.CubicalSingular.edge₁_cut₂ line 445
  124. theorem OAI.EilenbergGanea.CubicalSingular.edge₂_cut₂ line 447
  125. theorem OAI.EilenbergGanea.CubicalSingular.face₁_cut₃ line 449
  126. theorem OAI.EilenbergGanea.CubicalSingular.face₂_cut₃ line 451
  127. theorem OAI.EilenbergGanea.CubicalSingular.face₃_cut₃ line 453
  128. theorem OAI.EilenbergGanea.CubicalSingular.b₁_subdivision line 456
  129. theorem OAI.EilenbergGanea.CubicalSingular.b₂_subdivision line 461
  130. theorem OAI.EilenbergGanea.CubicalSingular.b₃_subdivision line 469
  131. theorem OAI.EilenbergGanea.CubicalSingular.cut₁_comp line 477
  132. theorem OAI.EilenbergGanea.CubicalSingular.cut₂_comp line 479
  133. theorem OAI.EilenbergGanea.CubicalSingular.cut₃_comp line 481
  134. theorem OAI.EilenbergGanea.CubicalSingular.S₁_push line 484
  135. theorem OAI.EilenbergGanea.CubicalSingular.S₂_push line 489
  136. theorem OAI.EilenbergGanea.CubicalSingular.S₃_push line 494
  137. theorem OAI.EilenbergGanea.CubicalSingular.cut₁_constant line 499
  138. theorem OAI.EilenbergGanea.CubicalSingular.cut₂_degenerate₁ line 501
  139. theorem OAI.EilenbergGanea.CubicalSingular.cut₂_degenerate₂ line 503
  140. theorem OAI.EilenbergGanea.CubicalSingular.S₁_D₁ line 506
  141. theorem OAI.EilenbergGanea.CubicalSingular.S₂_D₂ line 516
  142. def OAI.EilenbergGanea.CubicalSingular.SN₁ line 536
  143. def OAI.EilenbergGanea.CubicalSingular.SN₂ line 537
  144. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_mk line 538
  145. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_mk line 539
  146. theorem OAI.EilenbergGanea.CubicalSingular.d₁_subdivision line 541
  147. theorem OAI.EilenbergGanea.CubicalSingular.d₂_subdivision line 545
  148. theorem OAI.EilenbergGanea.CubicalSingular.d₃_subdivision line 550
  149. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_push line 554
  150. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_push line 559
  151. def OAI.EilenbergGanea.CubicalSingular.gen₁ line 569
  152. def OAI.EilenbergGanea.CubicalSingular.gen₂ line 570
  153. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_gen line 571
  154. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_gen line 574
  155. def OAI.EilenbergGanea.CubicalSingular.subdivisionFiller₁ line 581
  156. theorem OAI.EilenbergGanea.CubicalSingular.subdivisionFiller₁_boundary line 585
  157. def OAI.EilenbergGanea.CubicalSingular.H₁raw line 590
  158. theorem OAI.EilenbergGanea.CubicalSingular.H₁raw_single line 592
  159. theorem OAI.EilenbergGanea.CubicalSingular.H₁raw_D₁ line 595
  160. def OAI.EilenbergGanea.CubicalSingular.H₁ line 601
  161. theorem OAI.EilenbergGanea.CubicalSingular.H₁_mk line 602
  162. theorem OAI.EilenbergGanea.CubicalSingular.subdivision_homotopy₁ line 604
  163. theorem OAI.EilenbergGanea.CubicalSingular.H₁raw_push line 618
  164. theorem OAI.EilenbergGanea.CubicalSingular.H₁_push line 623
  165. def OAI.EilenbergGanea.CubicalSingular.subdivisionCycle₂ line 627
  166. theorem OAI.EilenbergGanea.CubicalSingular.subdivisionCycle₂_cycle line 631
  167. def OAI.EilenbergGanea.CubicalSingular.subdivisionFiller₂ line 634
  168. theorem OAI.EilenbergGanea.CubicalSingular.subdivisionFiller₂_boundary line 637
  169. def OAI.EilenbergGanea.CubicalSingular.H₂raw line 640
  170. theorem OAI.EilenbergGanea.CubicalSingular.H₂raw_single line 642
  171. theorem OAI.EilenbergGanea.CubicalSingular.subdivision_homotopy₂ line 645
  172. def OAI.EilenbergGanea.CubicalSingular.bad₁ line 666
  173. def OAI.EilenbergGanea.CubicalSingular.bad₂ line 667
  174. theorem OAI.EilenbergGanea.CubicalSingular.D₁_supported line 670
  175. theorem OAI.EilenbergGanea.CubicalSingular.D₂_supported line 678
  176. def OAI.EilenbergGanea.CubicalSingular.cubeSet line 687
  177. theorem OAI.EilenbergGanea.CubicalSingular.cubeSet_mono line 690
  178. theorem OAI.EilenbergGanea.CubicalSingular.cubeSet_inter line 693
  179. theorem OAI.EilenbergGanea.CubicalSingular.cubeSet_univ line 698
  180. def OAI.EilenbergGanea.CubicalSingular.inc line 701
  181. theorem OAI.EilenbergGanea.CubicalSingular.range_comp_inc line 703
  182. def OAI.EilenbergGanea.CubicalSingular.L₀ line 713
  183. def OAI.EilenbergGanea.CubicalSingular.raw₁ line 714
  184. def OAI.EilenbergGanea.CubicalSingular.raw₂ line 715
  185. def OAI.EilenbergGanea.CubicalSingular.L₁ line 716
  186. def OAI.EilenbergGanea.CubicalSingular.L₂ line 717
  187. def OAI.EilenbergGanea.CubicalSingular.L₃ line 718
  188. theorem OAI.EilenbergGanea.CubicalSingular.supported_quotient_inter line 720
  189. theorem OAI.EilenbergGanea.CubicalSingular.L₀_inter line 734
  190. theorem OAI.EilenbergGanea.CubicalSingular.L₁_inter line 735
  191. theorem OAI.EilenbergGanea.CubicalSingular.L₂_inter line 739
  192. theorem OAI.EilenbergGanea.CubicalSingular.L₃_inter line 743
  193. theorem OAI.EilenbergGanea.CubicalSingular.L₀_mono line 748
  194. theorem OAI.EilenbergGanea.CubicalSingular.L₁_mono line 749
  195. theorem OAI.EilenbergGanea.CubicalSingular.L₂_mono line 751
  196. theorem OAI.EilenbergGanea.CubicalSingular.L₃_mono line 753
  197. theorem OAI.EilenbergGanea.CubicalSingular.L₁_span line 755
  198. theorem OAI.EilenbergGanea.CubicalSingular.L₂_span line 759
  199. theorem OAI.EilenbergGanea.CubicalSingular.gen₁_mem line 763
  200. theorem OAI.EilenbergGanea.CubicalSingular.gen₂_mem line 766
  201. theorem OAI.EilenbergGanea.CubicalSingular.d₁_support line 770
  202. theorem OAI.EilenbergGanea.CubicalSingular.d₂_support line 779
  203. theorem OAI.EilenbergGanea.CubicalSingular.d₃_support line 793
  204. abbrev OAI.EilenbergGanea.NormalizedSupport.Chains line 817
  205. abbrev OAI.EilenbergGanea.NormalizedSupport.Q line 818
  206. def OAI.EilenbergGanea.NormalizedSupport.supported line 820
  207. theorem OAI.EilenbergGanea.NormalizedSupport.comap_supported line 823
  208. theorem OAI.EilenbergGanea.NormalizedSupport.supported_mono line 827
  209. theorem OAI.EilenbergGanea.NormalizedSupport.supported_inter line 830
  210. theorem OAI.EilenbergGanea.NormalizedSupport.supported_union line 839
  211. theorem OAI.EilenbergGanea.NormalizedSupport.supported_empty line 843
  212. theorem OAI.EilenbergGanea.NormalizedSupport.supported_univ line 845
  213. theorem OAI.EilenbergGanea.NormalizedSupport.mk_mem_supported line 848
  214. theorem OAI.EilenbergGanea.NormalizedSupport.mem_supported_mk line 852
  215. theorem OAI.EilenbergGanea.NormalizedSupport.exists_split line 867

    Source documentation

    The hypothesis is on actual normalized basis support, not homology.

    theorem exists_split (bad s t : Set A) {c : Q bad} (hc : c ∈ supported bad s ⊔ supported bad t) :
    ∃ a ∈ supported bad s, ∃ b ∈ supported bad t, a + b = c :=
…

    Mentions: OAI.EilenbergGanea.NormalizedSupport.Q, OAI.EilenbergGanea.NormalizedSupport.supported

  216. theorem OAI.EilenbergGanea.NormalizedSupport.comap_supported_of_injective line 873
  217. theorem OAI.EilenbergGanea.NormalizedSupport.normalized_injective line 882
  218. theorem OAI.EilenbergGanea.CubicalSingular.compose_injective line 896
  219. theorem OAI.EilenbergGanea.CubicalSingular.preimage_bad₁ line 901
  220. theorem OAI.EilenbergGanea.CubicalSingular.preimage_bad₂ line 914
  221. theorem OAI.EilenbergGanea.CubicalSingular.push₀_lmapDomain line 935
  222. theorem OAI.EilenbergGanea.CubicalSingular.push₁_lmapDomain line 941
  223. theorem OAI.EilenbergGanea.CubicalSingular.push₂_lmapDomain line 947
  224. theorem OAI.EilenbergGanea.CubicalSingular.push₃_lmapDomain line 953
  225. theorem OAI.EilenbergGanea.CubicalSingular.push₀_injective line 959
  226. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_injective line 964
  227. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_injective line 976
  228. theorem OAI.EilenbergGanea.CubicalSingular.range_push₁_inc line 988
  229. theorem OAI.EilenbergGanea.CubicalSingular.range_push₂_inc line 994
  230. theorem OAI.EilenbergGanea.CubicalSingular.range_push₃_inc line 1000
  231. theorem OAI.EilenbergGanea.CubicalSingular.range_pushN₁_inc line 1006
  232. theorem OAI.EilenbergGanea.CubicalSingular.range_pushN₂_inc line 1020
  233. theorem OAI.EilenbergGanea.CubicalSingular.pushN₁_support line 1034
  234. theorem OAI.EilenbergGanea.CubicalSingular.pushN₂_support line 1041
  235. theorem OAI.EilenbergGanea.CubicalSingular.push₃_support line 1048
  236. theorem OAI.EilenbergGanea.CubicalSingular.H₁_support line 1055
  237. theorem OAI.EilenbergGanea.CubicalSingular.H₂raw_support line 1063
  238. theorem OAI.EilenbergGanea.CubicalSingular.exact₁_on_contractible line 1071
  239. theorem OAI.EilenbergGanea.CubicalSingular.exact₂_on_contractible line 1084
  240. abbrev OAI.EilenbergGanea.CubicalMesh.Chains line 1104
  241. def OAI.EilenbergGanea.CubicalMesh.small line 1106
  242. def OAI.EilenbergGanea.CubicalMesh.subchains line 1107
  243. def OAI.EilenbergGanea.CubicalMesh.subdivision line 1109
  244. theorem OAI.EilenbergGanea.CubicalMesh.subdivision_single line 1113
  245. theorem OAI.EilenbergGanea.CubicalMesh.subdivision_preserves line 1118
  246. def OAI.EilenbergGanea.CubicalMesh.shrinking line 1130
  247. theorem OAI.EilenbergGanea.CubicalMesh.iterate_parametrized line 1134
  248. theorem OAI.EilenbergGanea.CubicalMesh.shrinking_small line 1164
  249. theorem OAI.EilenbergGanea.CubicalMesh.single_eventually_small line 1190
  250. theorem OAI.EilenbergGanea.CubicalMesh.chain_eventually_small line 1198
  251. theorem OAI.EilenbergGanea.CubicalSingular.half_dist line 1243
  252. theorem OAI.EilenbergGanea.CubicalSingular.interval_diameter line 1249
  253. def OAI.EilenbergGanea.CubicalSingular.half₂ line 1253
  254. def OAI.EilenbergGanea.CubicalSingular.half₃ line 1255
  255. theorem OAI.EilenbergGanea.CubicalSingular.half₂_dist line 1258
  256. theorem OAI.EilenbergGanea.CubicalSingular.half₃_dist line 1265
  257. theorem OAI.EilenbergGanea.CubicalSingular.S₁_mesh line 1273
  258. theorem OAI.EilenbergGanea.CubicalSingular.S₂_mesh line 1275
  259. theorem OAI.EilenbergGanea.CubicalSingular.S₃_mesh line 1281
  260. theorem OAI.EilenbergGanea.CubicalSingular.small_pair line 1287
  261. theorem OAI.EilenbergGanea.CubicalSingular.S₁_eventually_small line 1293
  262. theorem OAI.EilenbergGanea.CubicalSingular.S₂_eventually_small line 1301
  263. theorem OAI.EilenbergGanea.CubicalSingular.S₃_eventually_small line 1309
  264. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_iter_mk line 1318
  265. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_iter_mk line 1324
  266. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_eventually_small line 1330
  267. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_eventually_small line 1338
  268. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_support line 1346
  269. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_support line 1354
  270. theorem OAI.EilenbergGanea.CubicalSingular.S₃_support line 1362
  271. theorem OAI.EilenbergGanea.CubicalSingular.SN₁_iter_support line 1371
  272. theorem OAI.EilenbergGanea.CubicalSingular.SN₂_iter_support line 1376
  273. theorem OAI.EilenbergGanea.CubicalSingular.d₁_SN₁_iter line 1381
  274. theorem OAI.EilenbergGanea.CubicalSingular.d₂_SN₂_iter line 1386
  275. theorem OAI.EilenbergGanea.CubicalSingular.d₃_S₃_iter line 1391
  276. def OAI.EilenbergGanea.CubicalSingular.K₁ line 1396
  277. theorem OAI.EilenbergGanea.CubicalSingular.K₁_boundary line 1400
  278. theorem OAI.EilenbergGanea.CubicalSingular.K₁_support line 1408