OAI/Geometry/SingularHomology/ActualSingularSubdivision.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.ActualSingularSubdivision.identityChain line 17
  2. def OAI.Problem340.ActualSingularSubdivision.subdivisionChain line 21
  3. def OAI.Problem340.ActualSingularSubdivision.homotopyChain line 25
  4. def OAI.Problem340.ActualSingularSubdivision.subdivision line 29
  5. def OAI.Problem340.ActualSingularSubdivision.homotopyOperator line 33
  6. lemma OAI.Problem340.ActualSingularSubdivision.realize_standardVertices line 37
  7. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChain_zero line 48
  8. theorem OAI.Problem340.ActualSingularSubdivision.homotopyChain_zero line 52
  9. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChain_boundary_affine line 55
  10. theorem OAI.Problem340.ActualSingularSubdivision.homotopyChain_boundary_affine line 64
  11. theorem OAI.Problem340.ActualSingularSubdivision.subdivision_generator line 75
  12. theorem OAI.Problem340.ActualSingularSubdivision.homotopyOperator_generator line 82
  13. lemma OAI.Problem340.ActualSingularSubdivision.realize_eq_aux line 89
  14. lemma OAI.Problem340.ActualSingularSubdivision.realizeInSimplex_map line 96
  15. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChain_boundary line 104
  16. theorem OAI.Problem340.ActualSingularSubdivision.homotopyChain_boundary line 116
  17. theorem OAI.Problem340.ActualSingularSubdivision.subdivision_zero line 130
  18. lemma OAI.Problem340.ActualSingularSubdivision.realizeInSimplex_affineMap line 136
  19. theorem OAI.Problem340.ActualSingularSubdivision.subdivision_realize line 145
  20. theorem OAI.Problem340.ActualSingularSubdivision.subdivision_pow_realize line 163