OAI/Geometry/SingularHomology/IteratedSubdivision.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.IteratedSubdivision.eventuallyIn line 15
  2. theorem OAI.Problem340.IteratedSubdivision.pow_mem_of_mem line 28
  3. theorem OAI.Problem340.IteratedSubdivision.mem_eventuallyIn_of_pow_mem line 36
  4. theorem OAI.Problem340.IteratedSubdivision.finsupp_eventuallyIn line 45
  5. theorem OAI.Problem340.IteratedSubdivision.finsupp_exists_uniform_iteration line 56
  6. theorem OAI.Problem340.IteratedSubdivision.finite_family_uniform_iteration line 66
  7. def OAI.Problem340.IteratedSubdivision.chainIterate line 88
  8. def OAI.Problem340.IteratedSubdivision.iterateHomotopy line 92
  9. theorem OAI.Problem340.IteratedSubdivision.iterateHomotopy_hom line 97
  10. theorem OAI.Problem340.IteratedSubdivision.chainIterate_eq_pow line 107
  11. theorem OAI.Problem340.IteratedSubdivision.homologyMap_chainIterate line 113
  12. theorem OAI.Problem340.IteratedSubdivision.chainIterate_f_hom line 125
  13. theorem OAI.Problem340.IteratedSubdivision.chainIterate_preserves line 134
  14. theorem OAI.Problem340.IteratedSubdivision.iterateHomotopy_preserves line 141