OAI/GroupTheory/UniversalGroup/Milnor.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Milnor.complex line 16
  2. abbrev OAI.UniversalFInfinity.Milnor.Space line 22
  3. lemma OAI.UniversalFInfinity.Milnor.mem_complex line 24
  4. def OAI.UniversalFInfinity.Milnor.bounded line 27
  5. lemma OAI.UniversalFInfinity.Milnor.bounded_le line 34
  6. lemma OAI.UniversalFInfinity.Milnor.bounded_mono line 35
  7. lemma OAI.UniversalFInfinity.Milnor.map_face line 39
  8. def OAI.UniversalFInfinity.Milnor.map line 47
  9. lemma OAI.UniversalFInfinity.Milnor.map_comp line 50
  10. lemma OAI.UniversalFInfinity.Milnor.map_id line 57
  11. def OAI.UniversalFInfinity.Milnor.vertex line 61
  12. lemma OAI.UniversalFInfinity.Milnor.bounded_union_apex line 67
  13. lemma OAI.UniversalFInfinity.Milnor.bounded_id_face line 81
  14. lemma OAI.UniversalFInfinity.Milnor.bounded_const_face line 83
  15. lemma OAI.UniversalFInfinity.Milnor.bounded_contiguous line 87
  16. lemma OAI.UniversalFInfinity.Milnor.bounded_map_id line 92
  17. lemma OAI.UniversalFInfinity.Milnor.map_const_vertex line 98
  18. abbrev OAI.UniversalFInfinity.Simplicial.Cell line 113
  19. def OAI.UniversalFInfinity.Simplicial.cellOfFace line 115
  20. def OAI.UniversalFInfinity.Simplicial.cellEquiv line 118
  21. def OAI.UniversalFInfinity.Simplicial.faceDisk line 121
  22. lemma OAI.UniversalFInfinity.Simplicial.faceDisk_open line 124
  23. def OAI.UniversalFInfinity.Simplicial.diskMap line 129
  24. lemma OAI.UniversalFInfinity.Simplicial.diskMap_injective line 132
  25. lemma OAI.UniversalFInfinity.Simplicial.diskMap_range line 135
  26. def OAI.UniversalFInfinity.Simplicial.characteristic line 138
  27. lemma OAI.UniversalFInfinity.Simplicial.characteristic_disk line 142
  28. lemma OAI.UniversalFInfinity.Simplicial.characteristic_bijOn line 145
  29. def OAI.UniversalFInfinity.Simplicial.characteristicPE line 166
  30. lemma OAI.UniversalFInfinity.Simplicial.characteristicPE_open line 169
  31. lemma OAI.UniversalFInfinity.Simplicial.characteristicPE_closed line 173
  32. lemma OAI.UniversalFInfinity.Simplicial.characteristicPE_continuous line 183
  33. lemma OAI.UniversalFInfinity.Simplicial.characteristicPE_continuous_symm line 192
  34. lemma OAI.UniversalFInfinity.Simplicial.support_lt_of_sphere line 208
  35. lemma OAI.UniversalFInfinity.Simplicial.subcells_finite line 224
  36. def OAI.UniversalFInfinity.Simplicial.subcells line 232
  37. lemma OAI.UniversalFInfinity.Simplicial.characteristic_boundary line 234
  38. instance OAI.UniversalFInfinity.Simplicial.cwComplex line 254