OAI/Analysis/BoundedHochschild/FinitePaths.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous finite path tests and construction of stage assignments.

  1. def OAI.HochschildRare.signedValue line 29
  2. def OAI.HochschildRare.pathValue line 32
  3. def OAI.HochschildRare.FinitePathTests line 38
  4. def OAI.HochschildRare.assignedLabel line 50
  5. abbrev OAI.HochschildRare.StepCoeff line 55
  6. def OAI.HochschildRare.stepEmbedding line 56
  7. lemma OAI.HochschildRare.stepEmbedding_injective line 61
  8. lemma OAI.HochschildRare.goodPath_step_range line 87
  9. lemma OAI.HochschildRare.lift_pathValue line 102
  10. abbrev OAI.HochschildRare.StageTest line 115
  11. instance OAI.HochschildRare.stageTestFintype line 119
  12. def OAI.HochschildRare.encodePath line 127
  13. lemma OAI.HochschildRare.encodePath_decodes line 132
  14. lemma OAI.HochschildRare.encodePath_distinguished line 137
  15. def OAI.HochschildRare.stageCoeff line 151
  16. lemma OAI.HochschildRare.updated_step line 155
  17. lemma OAI.HochschildRare.pathValue_updated line 165
  18. def OAI.HochschildRare.AtStage line 182
  19. theorem OAI.HochschildRare.exists_stage_choice line 191
  20. lemma OAI.HochschildRare.atStage_congr line 208
  21. def OAI.HochschildRare.stageAssignments line 231
  22. lemma OAI.HochschildRare.stageAssignments_spec line 237
  23. lemma OAI.HochschildRare.stageAssignments_stable line 241
  24. theorem OAI.HochschildRare.exists_label_of_finite_paths line 251