OAI/Algebra/GroupRing/SimplexTopology.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingTopology.simplexSet line 9
  2. instance OAI.GroupRingTopology.(instance at line 13) line 13
  3. def OAI.GroupRingTopology.SimplexDisk.Truncated line 29
  4. def OAI.GroupRingTopology.SimplexDisk.Positive line 31
  5. def OAI.GroupRingTopology.SimplexDisk.sumCLM line 33
  6. lemma OAI.GroupRingTopology.SimplexDisk.sumCLM_apply line 35
  7. lemma OAI.GroupRingTopology.SimplexDisk.truncated_closed line 38
  8. lemma OAI.GroupRingTopology.SimplexDisk.positive_open line 45
  9. lemma OAI.GroupRingTopology.SimplexDisk.interior_truncated line 52
  10. lemma OAI.GroupRingTopology.SimplexDisk.truncated_convex line 74
  11. lemma OAI.GroupRingTopology.SimplexDisk.truncated_bounded line 81
  12. lemma OAI.GroupRingTopology.SimplexDisk.positive_nonempty line 87
  13. def OAI.GroupRingTopology.SimplexDisk.ambient line 94
  14. lemma OAI.GroupRingTopology.SimplexDisk.ambient_positive line 98
  15. lemma OAI.GroupRingTopology.SimplexDisk.ambient_truncated line 102
  16. def OAI.GroupRingTopology.SimplexDisk.truncatedDisk line 107
  17. def OAI.GroupRingTopology.SimplexDisk.simplexTruncated line 110
  18. def OAI.GroupRingTopology.SimplexDisk.simplexDisk line 140
  19. lemma OAI.GroupRingTopology.SimplexDisk.simplexTruncated_positive line 143
  20. lemma OAI.GroupRingTopology.SimplexDisk.simplexDisk_open line 157
  21. lemma OAI.GroupRingTopology.SimplexDisk.simplexDisk_boundary line 164
  22. def OAI.GroupRingTopology.SimplexDisk.reindex line 182
  23. lemma OAI.GroupRingTopology.SimplexDisk.reindex_positive line 191
  24. def OAI.GroupRingTopology.Simplicial.Space line 210

    Source documentation

    Finitely supported probability weights on a face, with the weak topology.

    def Space := {w : V →₀ ℝ | (∀ v, 0 ≤ w v) ∧ w.sum (fun _ r => r) = 1 ∧ w.support ∈ K}
  25. abbrev OAI.GroupRingTopology.Simplicial.Face line 211
  26. lemma OAI.GroupRingTopology.Simplicial.support_nonempty line 213
  27. lemma OAI.GroupRingTopology.Simplicial.face_nonempty line 221
  28. def OAI.GroupRingTopology.Simplicial.weight line 223
  29. lemma OAI.GroupRingTopology.Simplicial.weight_apply line 226
  30. lemma OAI.GroupRingTopology.Simplicial.weight_apply_not line 230
  31. lemma OAI.GroupRingTopology.Simplicial.weight_nonneg line 236
  32. lemma OAI.GroupRingTopology.Simplicial.weight_sum line 242
  33. lemma OAI.GroupRingTopology.Simplicial.weight_support_subset line 246
  34. def OAI.GroupRingTopology.Simplicial.faceMap line 252
  35. def OAI.GroupRingTopology.Simplicial.quotient line 256
  36. instance OAI.GroupRingTopology.Simplicial.(instance at line 258) line 258
  37. lemma OAI.GroupRingTopology.Simplicial.continuous_iff line 260
  38. lemma OAI.GroupRingTopology.Simplicial.continuous_faceMap line 265
  39. lemma OAI.GroupRingTopology.Simplicial.continuous_eval line 268
  40. instance OAI.GroupRingTopology.Simplicial.(instance at line 284) line 284
  41. lemma OAI.GroupRingTopology.Simplicial.faceMap_injective line 289
  42. lemma OAI.GroupRingTopology.Simplicial.faceMap_closedEmbedding line 296
  43. def OAI.GroupRingTopology.Simplicial.coordinates line 299
  44. lemma OAI.GroupRingTopology.Simplicial.faceMap_coordinates line 304
  45. lemma OAI.GroupRingTopology.Simplicial.range_faceMap line 314
  46. lemma OAI.GroupRingTopology.Simplicial.quotient_surjective line 322
  47. lemma OAI.GroupRingTopology.Simplicial.isClosed_iff line 327
  48. lemma OAI.GroupRingTopology.Simplicial.support_eq_iff line 332
  49. lemma OAI.GroupRingTopology.Simplicial.continuous_of_support_subset line 359
  50. lemma OAI.GroupRingTopology.Simplicial.push_apply line 369
  51. lemma OAI.GroupRingTopology.Simplicial.push_nonneg line 380
  52. lemma OAI.GroupRingTopology.Simplicial.push_sum line 386
  53. def OAI.GroupRingTopology.Simplicial.map line 390
  54. lemma OAI.GroupRingTopology.Simplicial.map_support line 397
  55. lemma OAI.GroupRingTopology.Simplicial.continuous_map line 402
  56. def OAI.GroupRingTopology.Simplicial.mapC line 425
  57. lemma OAI.GroupRingTopology.Simplicial.map_id line 428
  58. lemma OAI.GroupRingTopology.Simplicial.map_comp line 432
  59. lemma OAI.GroupRingTopology.Simplicial.quotient_quotientMap line 440
  60. lemma OAI.GroupRingTopology.Simplicial.continuous_prod_iff line 443