OAI/Dynamics/EntropyCounterexample/CoordinateGoodCover.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.CoordinateGoodCover.sphereSlice line 17
  2. theorem OAI.Problem340.CoordinateGoodCover.contractible_sphereSlice line 20
  3. def OAI.Problem340.CoordinateGoodCover.positiveCone line 63
  4. theorem OAI.Problem340.CoordinateGoodCover.convex_positiveCone line 66
  5. theorem OAI.Problem340.CoordinateGoodCover.positiveCone_smul line 72
  6. theorem OAI.Problem340.CoordinateGoodCover.zero_not_mem_positiveCone line 78
  7. theorem OAI.Problem340.CoordinateGoodCover.contractible_positiveSphere line 84
  8. theorem OAI.Problem340.CoordinateGoodCover.contractible_pi line 94
  9. structure OAI.Problem340.CoordinateGoodCover.GoodCover line 102
  10. theorem OAI.Problem340.CoordinateGoodCover.GoodCover.iUnion_eq_univ line 109
  11. def OAI.Problem340.CoordinateGoodCover.GoodCover.comap line 115
  12. theorem OAI.Problem340.CoordinateGoodCover.inter_prod_eq line 139
  13. def OAI.Problem340.CoordinateGoodCover.GoodCover.prod line 156
  14. def OAI.Problem340.CoordinateGoodCover.piSubsetHomeomorph line 179
  15. def OAI.Problem340.CoordinateGoodCover.GoodCover.pi line 194
  16. def OAI.Problem340.CoordinateGoodCover.signedCoordinate line 233
  17. def OAI.Problem340.CoordinateGoodCover.hemisphere line 236
  18. theorem OAI.Problem340.CoordinateGoodCover.isOpen_hemisphere line 239
  19. theorem OAI.Problem340.CoordinateGoodCover.hemisphere_covers line 242
  20. theorem OAI.Problem340.CoordinateGoodCover.hemisphere_inter_eq_slice line 259
  21. def OAI.Problem340.CoordinateGoodCover.sphereGoodCover line 265
  22. def OAI.Problem340.CoordinateGoodCover.clockSphereGoodCover line 276
  23. def OAI.Problem340.CoordinateGoodCover.counterexampleGoodCover line 280
  24. theorem OAI.Problem340.CoordinateGoodCover.card_counterexampleGoodCover_index line 285