OAI/GroupTheory/FiniteType/BoundaryValue.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryValue.A line 28
  2. def OAI.BoundaryValue.value line 31
  3. def OAI.BoundaryValue.boundary line 34
  4. lemma OAI.BoundaryValue.value_permute line 38
  5. lemma OAI.BoundaryValue.boundary_permutation line 42
  6. lemma OAI.BoundaryValue.value_const line 72
  7. lemma OAI.BoundaryValue.boundary_three line 75
  8. lemma OAI.BoundaryValue.boundary_three_at line 93
  9. def OAI.SimplexDegeneracy.append line 133
  10. lemma OAI.SimplexDegeneracy.append_castSucc line 135
  11. lemma OAI.SimplexDegeneracy.append_last line 137
  12. lemma OAI.SimplexDegeneracy.append_eq line 140
  13. lemma OAI.SimplexDegeneracy.append_face_last line 146
  14. lemma OAI.SimplexDegeneracy.append_face_last_castSucc line 150
  15. lemma OAI.SimplexDegeneracy.append_face_penult line 161
  16. def OAI.SimplexDegeneracy.degenerate line 188
  17. lemma OAI.SimplexDegeneracy.degenerate_face_last line 191
  18. lemma OAI.SimplexDegeneracy.degenerate_face_const line 196
  19. lemma OAI.SimplexDegeneracy.degenerate_standard_face line 207
  20. lemma OAI.SimplexDegeneracy.degenerate_twisted_face line 212
  21. lemma OAI.SimplexHorn.compatible_of_ordered line 227