OAI/GroupTheory/SimpleAmenable/CentralCovers/FormalLaws.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.smallActualModel_pullback line 20
  2. theorem OAI.SimpleAmenable.InitialCoverSystem.smallPrimitive_formal_of_actual line 35
  3. def OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.primitiveStar line 59
  4. def OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.starFamily line 65
  5. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.starFamily_small line 70
  6. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.starFamily_supported line 82
  7. def OAI.SimpleAmenable.oneSlopeCoordinates line 100
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.primitive_self_formal_law line 113
  9. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.oneSlope_pairs_formal_law line 129
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.starFamily_formal_table line 172
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.oneSlope_formal_table line 191