OAI/GroupTheory/SimpleAmenable/Configurations/StageFiberSum.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberSumFun line 15
  2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberSum line 22
  3. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberSum_inl line 42
  4. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberSum_inr line 44
  5. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.E line 47
  6. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.enumerate line 48
  7. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.E_map_enum line 49
  8. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.mu line 53
  9. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.mu_inl line 57
  10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.mu_inr line 65
  11. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberMap_sum_inl line 73
  12. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberMap_sum_inr line 79
  13. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberEmpty line 94
  14. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.eps line 96
  15. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberMap_id line 98
  16. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.mu_natural line 100
  17. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_assoc_left line 117
  18. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_assoc_mid line 123
  19. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_assoc_right line 129
  20. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_left line 135
  21. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_right line 139
  22. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_swap_left line 143
  23. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiber_swap_right line 147