OAI/GroupTheory/FiniteType/CWWhitehead.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CWWhitehead.Stage line 17
  2. def OAI.CWWhitehead.cellSide line 24
  3. theorem OAI.CWWhitehead.exists_cell_extension line 28
  4. theorem OAI.CWWhitehead.exists_next line 47
  5. def OAI.CWWhitehead.next line 75
  6. theorem OAI.CWWhitehead.next_compat line 78
  7. def OAI.CWWhitehead.emptyStage line 82
  8. def OAI.CWWhitehead.build line 88
  9. theorem OAI.CWWhitehead.build_compat line 92
  10. def OAI.CWWhitehead.allPaths line 96
  11. theorem OAI.CWWhitehead.allPaths_zero line 99
  12. theorem OAI.CWWhitehead.allPaths_one line 106
  13. def OAI.CWWhitehead.homotopy line 113
  14. theorem OAI.CWWhitehead.contractible_subtype line 119
  15. lemma OAI.SequentialCoreTower.sphereFill line 148
  16. lemma OAI.SequentialCoreTower.contractible line 177
  17. def OAI.SimpleFInftyOvergroups.HasTypeFInfty line 202

    Also declared: ComparatorChallenges/SimpleOvergroups.lean:16 (same declaration text).