OAI/Analysis/SphereIsometry/SubdivisionData.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The concrete recursively iterated subdivision of a finite simplex

  1. structure OAI.Tingley.CarrierComplex line 11
  2. def OAI.Tingley.CarrierComplex.sd line 24
  3. def OAI.Tingley.CarrierComplex.initial line 29
  4. def OAI.Tingley.iterData line 36
  5. abbrev OAI.Tingley.IterVertex line 40
  6. def OAI.Tingley.iterComplex line 42
  7. def OAI.Tingley.iterCarrier line 45
  8. def OAI.Tingley.topCells line 48
  9. def OAI.Tingley.codimFaces line 51
  10. def OAI.Tingley.faceCarrier line 54
  11. def OAI.Tingley.incidentTop line 57
  12. theorem OAI.Tingley.mem_topCells line 61
  13. theorem OAI.Tingley.mem_codimFaces line 65
  14. theorem OAI.Tingley.mem_incidentTop line 69
  15. theorem OAI.Tingley.iterComplex_empty_mem line 74
  16. theorem OAI.Tingley.iterComplex_down_closed line 77
  17. theorem OAI.Tingley.iterData_carrier_nonempty line 81
  18. theorem OAI.Tingley.iterData_card_le_carrier line 87
  19. theorem OAI.Tingley.iter_card_le_carrier line 100
  20. theorem OAI.Tingley.iter_card_le line 104
  21. theorem OAI.Tingley.top_faceCarrier line 109
  22. theorem OAI.Tingley.codim_faceCarrier_card line 115