OAI/GroupTheory/UniversalGroup/SimplexDisk.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

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