OAI/GroupTheory/FiniteType/AffineSimplex.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AffineSimplex.linear line 14
  2. def OAI.AffineSimplex.simplex line 19
  3. lemma OAI.AffineSimplex.simplex_apply line 23
  4. lemma OAI.AffineSimplex.simplex_mem_convex line 26
  5. lemma OAI.AffineSimplex.simplex_mem_hull line 30
  6. lemma OAI.AffineSimplex.linear_map line 34
  7. lemma OAI.AffineSimplex.simplex_map line 47
  8. lemma OAI.AffineSimplex.simplex_vertex line 58
  9. lemma OAI.AffineSimplex.simplex_basis line 62
  10. abbrev OAI.ConvexSimplex.Std line 71
  11. def OAI.ConvexSimplex.affine line 73
  12. lemma OAI.ConvexSimplex.affine_coe line 90
  13. lemma OAI.ConvexSimplex.affine_vertex line 93
  14. lemma OAI.ConvexSimplex.affine_id line 98
  15. lemma OAI.ConvexSimplex.affine_map line 105
  16. lemma OAI.ConvexSimplex.affine_comp line 113
  17. def OAI.ConvexSimplex.center line 129
  18. lemma OAI.ConvexSimplex.affine_center line 132
  19. lemma OAI.ConvexSimplex.center_coe line 136
  20. lemma OAI.ConvexSimplex.stdMap_affine line 140
  21. lemma OAI.ConvexSimplex.stdMap_center line 145
  22. abbrev OAI.SingularChains.Std line 157
  23. abbrev OAI.SingularChains.singular line 158
  24. abbrev OAI.SingularChains.chains line 159
  25. def OAI.SingularChains.simplex line 164
  26. def OAI.SingularChains.unsimplex line 167
  27. lemma OAI.SingularChains.simplex_unsimplex line 170
  28. lemma OAI.SingularChains.unsimplex_simplex line 172
  29. def OAI.SingularChains.face line 175
  30. lemma OAI.SingularChains.simplex_face line 178
  31. lemma OAI.SingularChains.simplex_map line 181
  32. def OAI.SingularChains.generator line 184
  33. lemma OAI.SingularChains.generator_boundary line 187
  34. def OAI.SingularChains.map line 192
  35. lemma OAI.SingularChains.generator_map line 195
  36. def OAI.SingularChains.desc line 199
  37. lemma OAI.SingularChains.generator_desc line 202
  38. lemma OAI.SingularChains.hom_ext line 207
  39. lemma OAI.SingularChains.map_comp line 213
  40. lemma OAI.SingularChains.map_id line 220
  41. def OAI.AffineRealization.singular line 233
  42. def OAI.AffineRealization.realize line 243
  43. lemma OAI.AffineRealization.generator_realize line 246
  44. lemma OAI.AffineRealization.realize_affine line 251
  45. def OAI.AffineRealization.basis line 259
  46. lemma OAI.AffineRealization.basis_map_face line 261
  47. lemma OAI.AffineRealization.basis_affine line 266
  48. lemma OAI.AffineRealization.basis_map_affine line 269
  49. lemma OAI.AffineRealization.face_affine line 277
  50. lemma OAI.AffineRealization.realize_face line 282