OAI/GroupTheory/FiniteType/BasedComplex.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BasedComplex.Data line 8
  2. lemma OAI.BasedComplex.d_vertex line 19
  3. lemma OAI.BasedComplex.linear_eq_on_support line 27
  4. structure OAI.BasedComplex.Contraction line 39
  5. def OAI.BasedComplex.extendBasis line 51
  6. def OAI.BasedComplex.extend line 60
  7. lemma OAI.BasedComplex.extend_single line 63
  8. lemma OAI.BasedComplex.extend_vertex line 67
  9. lemma OAI.BasedComplex.extend_positive line 71
  10. lemma OAI.BasedComplex.aug_extend line 80
  11. theorem OAI.BasedComplex.d_extend line 93
  12. lemma OAI.BasedComplex.map_mem_of_support line 118
  13. theorem OAI.BasedComplex.extend_mem line 129
  14. theorem OAI.BasedComplex.extend_degree line 152
  15. def OAI.BasedComplex.homotopyBasis line 177
  16. def OAI.BasedComplex.homotopy line 186
  17. lemma OAI.BasedComplex.homotopy_equation line 189
  18. lemma OAI.BasedComplex.aug_homotopy line 199
  19. theorem OAI.BasedComplex.d_homotopy line 208
  20. lemma OAI.BasedComplex.homotopy_mem line 248
  21. theorem OAI.BasedComplex.homotopy_degree line 270