OAI/GroupTheory/UniversalGroup/Simplicial.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Simplicial.Space line 15
  2. abbrev OAI.UniversalFInfinity.Simplicial.Face line 16
  3. lemma OAI.UniversalFInfinity.Simplicial.support_nonempty line 18
  4. lemma OAI.UniversalFInfinity.Simplicial.face_nonempty line 26
  5. def OAI.UniversalFInfinity.Simplicial.weight line 28
  6. lemma OAI.UniversalFInfinity.Simplicial.weight_apply line 31
  7. lemma OAI.UniversalFInfinity.Simplicial.weight_apply_not line 35
  8. lemma OAI.UniversalFInfinity.Simplicial.weight_nonneg line 41
  9. lemma OAI.UniversalFInfinity.Simplicial.weight_sum line 47
  10. lemma OAI.UniversalFInfinity.Simplicial.weight_support_subset line 51
  11. def OAI.UniversalFInfinity.Simplicial.faceMap line 57
  12. def OAI.UniversalFInfinity.Simplicial.quotient line 61
  13. instance OAI.UniversalFInfinity.Simplicial.(instance at line 63) line 63
  14. lemma OAI.UniversalFInfinity.Simplicial.continuous_iff line 65
  15. lemma OAI.UniversalFInfinity.Simplicial.continuous_faceMap line 70
  16. lemma OAI.UniversalFInfinity.Simplicial.continuous_eval line 73
  17. instance OAI.UniversalFInfinity.Simplicial.(instance at line 89) line 89
  18. lemma OAI.UniversalFInfinity.Simplicial.faceMap_injective line 94
  19. lemma OAI.UniversalFInfinity.Simplicial.faceMap_closedEmbedding line 101
  20. def OAI.UniversalFInfinity.Simplicial.coordinates line 104
  21. lemma OAI.UniversalFInfinity.Simplicial.faceMap_coordinates line 109
  22. lemma OAI.UniversalFInfinity.Simplicial.range_faceMap line 119
  23. lemma OAI.UniversalFInfinity.Simplicial.quotient_surjective line 127
  24. lemma OAI.UniversalFInfinity.Simplicial.isClosed_iff line 132
  25. lemma OAI.UniversalFInfinity.Simplicial.support_eq_iff line 137
  26. lemma OAI.UniversalFInfinity.Simplicial.continuous_of_support_subset line 165
  27. lemma OAI.UniversalFInfinity.Simplicial.push_apply line 175
  28. lemma OAI.UniversalFInfinity.Simplicial.push_nonneg line 186
  29. lemma OAI.UniversalFInfinity.Simplicial.push_sum line 192
  30. def OAI.UniversalFInfinity.Simplicial.map line 196
  31. lemma OAI.UniversalFInfinity.Simplicial.map_support line 203
  32. lemma OAI.UniversalFInfinity.Simplicial.continuous_map line 208
  33. def OAI.UniversalFInfinity.Simplicial.mapC line 231
  34. lemma OAI.UniversalFInfinity.Simplicial.map_id line 234
  35. lemma OAI.UniversalFInfinity.Simplicial.map_comp line 238
  36. lemma OAI.UniversalFInfinity.Simplicial.quotient_quotientMap line 246
  37. lemma OAI.UniversalFInfinity.Simplicial.continuous_prod_iff line 249
  38. def OAI.UniversalFInfinity.Simplicial.mass line 283
  39. lemma OAI.UniversalFInfinity.Simplicial.mass_apply line 284
  40. lemma OAI.UniversalFInfinity.Simplicial.blend_support line 286
  41. def OAI.UniversalFInfinity.Simplicial.blend line 290
  42. lemma OAI.UniversalFInfinity.Simplicial.blend_zero line 302
  43. lemma OAI.UniversalFInfinity.Simplicial.blend_one line 306
  44. lemma OAI.UniversalFInfinity.Simplicial.blend_self line 310
  45. def OAI.UniversalFInfinity.Simplicial.straight line 319
  46. lemma OAI.UniversalFInfinity.Simplicial.continuous_straight line 325
  47. def OAI.UniversalFInfinity.Simplicial.straightHomotopy line 342
  48. lemma OAI.UniversalFInfinity.Simplicial.straightHomotopy_fixed line 348
  49. def OAI.UniversalFInfinity.Simplicial.inclusion line 359
  50. lemma OAI.UniversalFInfinity.Simplicial.inclusion_injective line 361
  51. lemma OAI.UniversalFInfinity.Simplicial.inclusion_faceMap line 364
  52. lemma OAI.UniversalFInfinity.Simplicial.continuous_inclusion line 367
  53. lemma OAI.UniversalFInfinity.Simplicial.inclusion_isClosedMap line 372
  54. lemma OAI.UniversalFInfinity.Simplicial.inclusion_closedEmbedding line 406