OAI/GroupTheory/SimpleAmenable/Configurations/PolygonComponentStable.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.PolygonTracks.componentGenerator line 15
  2. lemma OAI.SimpleAmenable.PolygonTracks.componentGenerator_cofinal line 16
  3. def OAI.SimpleAmenable.PolygonTracks.standardFiber line 23
  4. def OAI.SimpleAmenable.PolygonTracks.standardNerveInclusion line 25
  5. lemma OAI.SimpleAmenable.PolygonTracks.standardNerveInclusion_obj line 29
  6. lemma OAI.SimpleAmenable.PolygonTracks.standardNerveInclusion_map line 31
  7. def OAI.SimpleAmenable.PolygonTracks.standardFiberInclusion line 33
  8. def OAI.SimpleAmenable.PolygonTracks.standardHomologyIso line 37
  9. lemma OAI.SimpleAmenable.PolygonObject.eqToHom_coord line 48
  10. lemma OAI.SimpleAmenable.PolygonObject.standardTensor_map line 51
  11. def OAI.SimpleAmenable.PolygonObject.standardTensorIso line 114
  12. def OAI.SimpleAmenable.PolygonObject.standardCastIso line 120
  13. def OAI.SimpleAmenable.PolygonObject.standardSuccessorIso line 124
  14. instance OAI.SimpleAmenable.PolygonTracks.standardFiberInclusion_faithful line 134
  15. instance OAI.SimpleAmenable.PolygonTracks.standardFiberInclusion_full line 137
  16. instance OAI.SimpleAmenable.PolygonTracks.standardFiberInclusion_essSurj line 141
  17. instance OAI.SimpleAmenable.PolygonTracks.standardFiberInclusion_isEquivalence line 143
  18. def OAI.SimpleAmenable.PolygonTracks.representativeGeneratorIso line 145
  19. def OAI.SimpleAmenable.PolygonTracks.representativeSuccessorIso line 147
  20. def OAI.SimpleAmenable.PolygonTracks.fiberSuccessorIso line 153
  21. lemma OAI.SimpleAmenable.PolygonTracks.component_successor_isIso line 161