OAI/GroupTheory/SimpleAmenable/Configurations/PointFiberEvaluation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.Fiber line 12
  2. instance OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.(instance at line 15) line 15
  3. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberMap line 22
  4. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.evaluation line 37
  5. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberSumFun line 69
  6. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberSum line 76
  7. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberSum_inl line 96
  8. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberSum_inr line 98
  9. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.E line 101
  10. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.enumerate line 102
  11. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.E_map_enum line 103
  12. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.mu line 107
  13. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.mu_inl line 111
  14. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.mu_inr line 119
  15. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberMap_sum_inl line 127
  16. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberMap_sum_inr line 133
  17. instance OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberEmpty line 148
  18. def OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.eps line 150
  19. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiberMap_id line 152
  20. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.mu_natural line 154
  21. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_assoc_left line 171
  22. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_assoc_mid line 177
  23. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_assoc_right line 183
  24. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_left line 189
  25. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_right line 193
  26. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_swap_left line 197
  27. lemma OAI.SimpleAmenable.PolygonObject.Labelled.PointFiber.fiber_swap_right line 201