OAI/Algebra/GroupRing/Simplicial.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingTopology.Simplicial.mass line 19
  2. lemma OAI.GroupRingTopology.Simplicial.mass_apply line 20
  3. lemma OAI.GroupRingTopology.Simplicial.blend_support line 22
  4. def OAI.GroupRingTopology.Simplicial.blend line 26
  5. lemma OAI.GroupRingTopology.Simplicial.blend_zero line 38
  6. lemma OAI.GroupRingTopology.Simplicial.blend_one line 42
  7. lemma OAI.GroupRingTopology.Simplicial.blend_self line 46
  8. def OAI.GroupRingTopology.Simplicial.straight line 55
  9. lemma OAI.GroupRingTopology.Simplicial.continuous_straight line 61
  10. def OAI.GroupRingTopology.Simplicial.straightHomotopy line 78
  11. lemma OAI.GroupRingTopology.Simplicial.straightHomotopy_fixed line 84
  12. def OAI.GroupRingTopology.Simplicial.inclusion line 95
  13. lemma OAI.GroupRingTopology.Simplicial.inclusion_injective line 97
  14. lemma OAI.GroupRingTopology.Simplicial.inclusion_faceMap line 100
  15. lemma OAI.GroupRingTopology.Simplicial.continuous_inclusion line 103
  16. lemma OAI.GroupRingTopology.Simplicial.inclusion_isClosedMap line 108
  17. lemma OAI.GroupRingTopology.Simplicial.inclusion_closedEmbedding line 142
  18. def OAI.GroupRingTopology.Milnor.complex line 153
  19. abbrev OAI.GroupRingTopology.Milnor.Space line 159
  20. lemma OAI.GroupRingTopology.Milnor.mem_complex line 161
  21. def OAI.GroupRingTopology.Milnor.bounded line 164
  22. lemma OAI.GroupRingTopology.Milnor.bounded_le line 171
  23. lemma OAI.GroupRingTopology.Milnor.bounded_mono line 172
  24. lemma OAI.GroupRingTopology.Milnor.map_face line 176
  25. def OAI.GroupRingTopology.Milnor.map line 184
  26. lemma OAI.GroupRingTopology.Milnor.map_comp line 187
  27. lemma OAI.GroupRingTopology.Milnor.map_id line 194
  28. def OAI.GroupRingTopology.Milnor.vertex line 198
  29. lemma OAI.GroupRingTopology.Milnor.bounded_union_apex line 204
  30. lemma OAI.GroupRingTopology.Milnor.bounded_id_face line 218
  31. lemma OAI.GroupRingTopology.Milnor.bounded_const_face line 220
  32. lemma OAI.GroupRingTopology.Milnor.bounded_contiguous line 224
  33. lemma OAI.GroupRingTopology.Milnor.bounded_map_id line 229
  34. lemma OAI.GroupRingTopology.Milnor.map_const_vertex line 235
  35. abbrev OAI.GroupRingTopology.Simplicial.Cell line 250
  36. def OAI.GroupRingTopology.Simplicial.cellOfFace line 252
  37. def OAI.GroupRingTopology.Simplicial.cellEquiv line 255
  38. def OAI.GroupRingTopology.Simplicial.faceDisk line 258
  39. lemma OAI.GroupRingTopology.Simplicial.faceDisk_open line 261
  40. def OAI.GroupRingTopology.Simplicial.diskMap line 266
  41. lemma OAI.GroupRingTopology.Simplicial.diskMap_injective line 269
  42. lemma OAI.GroupRingTopology.Simplicial.diskMap_range line 272
  43. def OAI.GroupRingTopology.Simplicial.characteristic line 275
  44. lemma OAI.GroupRingTopology.Simplicial.characteristic_disk line 279
  45. lemma OAI.GroupRingTopology.Simplicial.characteristic_bijOn line 282
  46. def OAI.GroupRingTopology.Simplicial.characteristicPE line 303
  47. lemma OAI.GroupRingTopology.Simplicial.characteristicPE_open line 306
  48. lemma OAI.GroupRingTopology.Simplicial.characteristicPE_closed line 310
  49. lemma OAI.GroupRingTopology.Simplicial.characteristicPE_continuous line 320
  50. lemma OAI.GroupRingTopology.Simplicial.characteristicPE_continuous_symm line 329
  51. lemma OAI.GroupRingTopology.Simplicial.support_lt_of_sphere line 345
  52. lemma OAI.GroupRingTopology.Simplicial.subcells_finite line 361
  53. def OAI.GroupRingTopology.Simplicial.subcells line 369
  54. lemma OAI.GroupRingTopology.Simplicial.characteristic_boundary line 371
  55. instance OAI.GroupRingTopology.Simplicial.cwComplex line 391