OAI/GroupTheory/FiniteType/SingularSubdivision.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingularSubdivision.sd line 13
  2. def OAI.SingularSubdivision.simplexChain line 15
  3. def OAI.SingularSubdivision.prismChain line 18
  4. lemma OAI.SingularSubdivision.simplexChain_affine line 21
  5. lemma OAI.SingularSubdivision.prismChain_affine line 28
  6. lemma OAI.SingularSubdivision.simplexChain_face line 35
  7. lemma OAI.SingularSubdivision.prismChain_face line 41
  8. lemma OAI.SingularSubdivision.simplexChain_boundary line 47
  9. lemma OAI.SingularSubdivision.prismChain_boundary line 55
  10. def OAI.SingularSubdivision.subdiv line 68
  11. lemma OAI.SingularSubdivision.generator_subdiv line 71
  12. lemma OAI.SingularSubdivision.generator_affine_subdiv line 76
  13. lemma OAI.SingularSubdivision.subdiv_comm line 81
  14. def OAI.SingularSubdivision.subdivision line 99
  15. def OAI.SingularSubdivision.prism line 107
  16. lemma OAI.SingularSubdivision.generator_prism line 110
  17. lemma OAI.SingularSubdivision.subdiv_zero line 115
  18. lemma OAI.SingularSubdivision.prism_zero line 121
  19. lemma OAI.SingularSubdivision.prism_boundary line 126
  20. lemma OAI.SingularSubdivision.subdiv_map line 147
  21. lemma OAI.SingularSubdivision.prism_map line 154
  22. def OAI.SingularSubdivision.homComponent line 161
  23. lemma OAI.SingularSubdivision.homComponent_succ line 164
  24. def OAI.SingularSubdivision.chainHomotopy line 167
  25. abbrev OAI.AffineSupport.gen line 190
  26. def OAI.AffineSupport.span line 192
  27. lemma OAI.AffineSupport.gen_mem line 195
  28. lemma OAI.AffineSupport.span_mono line 198
  29. lemma OAI.AffineSupport.map_mem line 203
  30. lemma OAI.AffineSupport.induction_on line 213
  31. lemma OAI.AffineSupport.map_gen line 232
  32. lemma OAI.AffineSupport.cone_gen line 237
  33. lemma OAI.AffineSupport.boundary_gen line 242
  34. lemma OAI.AffineSupport.subdiv_gen line 249