OAI/Analysis/SphereIsometry/FiniteComplex.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite complexes and their actual face-chain subdivision

The empty face is included. A subdivision vertex is always a nonempty old face, and a subdivision face is an actual finite inclusion-chain.

  1. structure OAI.Tingley.FiniteComplex line 20
  2. def OAI.Tingley.FiniteComplex.full line 29
  3. theorem OAI.Tingley.FiniteComplex.mem_full line 34
  4. abbrev OAI.Tingley.FiniteComplex.FaceVertex line 37
  5. instance OAI.Tingley.FiniteComplex.(instance at line 40) line 40
  6. def OAI.Tingley.FiniteComplex.chain line 45
  7. theorem OAI.Tingley.FiniteComplex.chain_mono line 48
  8. def OAI.Tingley.FiniteComplex.sd line 52
  9. theorem OAI.Tingley.FiniteComplex.mem_sd_iff line 62
  10. def OAI.Tingley.FiniteComplex.topCells line 67
  11. def OAI.Tingley.FiniteComplex.codimFaces line 70
  12. def OAI.Tingley.FiniteComplex.incidentTop line 73
  13. theorem OAI.Tingley.FiniteComplex.mem_topCells line 76
  14. theorem OAI.Tingley.FiniteComplex.mem_codimFaces line 80
  15. theorem OAI.Tingley.FiniteComplex.mem_incidentTop line 84
  16. def OAI.Tingley.FiniteComplex.CardBound line 89
  17. def OAI.Tingley.FiniteComplex.Pure line 92
  18. theorem OAI.Tingley.FiniteComplex.Pure.cardBound line 95
  19. def OAI.Tingley.FiniteComplex.faceCarrier line 103
  20. theorem OAI.Tingley.FiniteComplex.mem_faceCarrier line 107
  21. theorem OAI.Tingley.FiniteComplex.faceCarrier_mono line 112
  22. theorem OAI.Tingley.FiniteComplex.faceCarrier_empty line 117
  23. theorem OAI.Tingley.FiniteComplex.faceCarrier_singleton line 121
  24. def OAI.Tingley.FiniteComplex.sdCarrier line 125
  25. theorem OAI.Tingley.FiniteComplex.sdCarrier_nonempty line 128