OAI/Dynamics/EntropyCounterexample/CircleWindingCocycle.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.CircleWinding.CircleSpace line 13
  2. abbrev OAI.Problem340.CircleWinding.singularSet line 14
  3. abbrev OAI.Problem340.CircleWinding.coefficients line 15
  4. abbrev OAI.Problem340.CircleWinding.chains line 16
  5. def OAI.Problem340.CircleWinding.cochainOfIncrement line 18
  6. theorem OAI.Problem340.CircleWinding.generator_cochainOfIncrement line 21
  7. theorem OAI.Problem340.CircleWinding.cochainOfIncrement_boundary line 27
  8. def OAI.Problem340.CircleWinding.simplexIncrement line 38
  9. lemma OAI.Problem340.CircleWinding.simplexIncrement_face line 43
  10. lemma OAI.Problem340.CircleWinding.simplexIncrement_triangle line 53
  11. def OAI.Problem340.CircleWinding.windingCochain line 59
  12. theorem OAI.Problem340.CircleWinding.boundary_windingCochain line 62
  13. theorem OAI.Problem340.CircleWinding.windingCochain_boundary line 65
  14. theorem OAI.Problem340.CircleWinding.simplexIncrement_loop line 69
  15. theorem OAI.Problem340.CircleWinding.windingCochain_loop line 78
  16. theorem OAI.Problem340.CircleWinding.loop_not_boundary line 85