OAI/Geometry/SingularHomology/AffineSimplexGeometry.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.AffineSimplex.face line 12
  2. def OAI.Problem340.AffineSimplex.cone line 15
  3. lemma OAI.Problem340.AffineSimplex.cone_zero line 17
  4. lemma OAI.Problem340.AffineSimplex.cone_succ line 20
  5. lemma OAI.Problem340.AffineSimplex.face_zero_cone line 24
  6. lemma OAI.Problem340.AffineSimplex.face_succ_cone line 29
  7. lemma OAI.Problem340.AffineSimplex.range_cone line 36
  8. def OAI.Problem340.AffineSimplex.realize line 45
  9. lemma OAI.Problem340.AffineSimplex.realize_vertex line 48
  10. lemma OAI.Problem340.AffineSimplex.realize_cone line 52
  11. lemma OAI.Problem340.AffineSimplex.realize_comp_map line 56
  12. lemma OAI.Problem340.AffineSimplex.realize_face line 72
  13. lemma OAI.Problem340.AffineSimplex.realize_mem line 77
  14. lemma OAI.Problem340.AffineSimplex.realize_mem_convexHull line 82
  15. lemma OAI.Problem340.AffineSimplex.realize_cone_mem_convexHull line 87
  16. def OAI.Problem340.AffineSimplex.barycenter line 96
  17. lemma OAI.Problem340.AffineSimplex.barycenter_mem_convexHull line 98
  18. lemma OAI.Problem340.AffineSimplex.barycenter_eq_sum line 102
  19. lemma OAI.Problem340.AffineSimplex.continuous_realize line 110
  20. def OAI.Problem340.AffineSimplex.realizeMap line 115
  21. lemma OAI.Problem340.AffineSimplex.realizeMap_apply line 118
  22. lemma OAI.Problem340.AffineSimplex.realizeMap_comp_map line 121
  23. def OAI.Problem340.AffineSimplex.realizeIn line 127
  24. lemma OAI.Problem340.AffineSimplex.realizeIn_coe line 132
  25. def OAI.Problem340.AffineSimplex.simplexRealizeMap line 144
  26. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_coe line 152
  27. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_apply line 156
  28. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_vertex line 161
  29. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_comp_map line 166
  30. lemma OAI.Problem340.AffineSimplex.map_simplexRealizeMap line 176
  31. lemma OAI.Problem340.AffineSimplex.realize_simplexRealizeMap line 189
  32. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_assoc line 196
  33. def OAI.Problem340.AffineSimplex.simplexBarycenter line 206
  34. lemma OAI.Problem340.AffineSimplex.simplexBarycenter_coe line 209
  35. lemma OAI.Problem340.AffineSimplex.simplexRealizeMap_barycenter line 213
  36. lemma OAI.Problem340.AffineSimplex.map_simplexBarycenter line 219
  37. lemma OAI.Problem340.AffineSimplex.simplexBarycenter_mem_convexHull line 224