OAI/Dynamics/EntropyCounterexample/SphereCoverGeometry.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SphereCover.northComplement line 14
  2. def OAI.Problem340.SphereCover.southComplement line 16
  3. lemma OAI.Problem340.SphereCover.south_ne_north line 18
  4. lemma OAI.Problem340.SphereCover.isOpen_northComplement line 21
  5. lemma OAI.Problem340.SphereCover.isOpen_southComplement line 23
  6. lemma OAI.Problem340.SphereCover.cover line 25
  7. def OAI.Problem340.SphereCover.northHomeomorph line 33
  8. def OAI.Problem340.SphereCover.flipHomeomorph line 41
  9. def OAI.Problem340.SphereCover.southToNorthHomeomorph line 49
  10. def OAI.Problem340.SphereCover.southHomeomorph line 61
  11. instance OAI.Problem340.SphereCover.north_contractible line 64
  12. instance OAI.Problem340.SphereCover.south_contractible line 67
  13. lemma OAI.Problem340.SphereCover.north_homology_subsingleton line 70
  14. lemma OAI.Problem340.SphereCover.south_homology_subsingleton line 74
  15. abbrev OAI.Problem340.SphereCover.PuncturedPlane line 78
  16. def OAI.Problem340.SphereCover.overlapHomeomorph line 80
  17. abbrev OAI.Problem340.SphereCover.ComplexCircle line 97
  18. def OAI.Problem340.SphereCover.radialRetraction line 99
  19. def OAI.Problem340.SphereCover.circleInclusion line 108
  20. lemma OAI.Problem340.SphereCover.radialRetraction_circleInclusion line 112
  21. lemma OAI.Problem340.SphereCover.radial_coefficient_pos line 119
  22. def OAI.Problem340.SphereCover.radialHomotopy line 129
  23. def OAI.Problem340.SphereCover.puncturedPlaneEquivCircle line 150
  24. def OAI.Problem340.SphereCover.overlapEquivCircle line 161
  25. lemma OAI.Problem340.SphereCover.radialHomotopy_fixes_circle line 164
  26. def OAI.Problem340.SphereCover.circleHomeomorphClock line 171
  27. def OAI.Problem340.SphereCover.overlapEquivClock line 177
  28. def OAI.Problem340.SphereCover.overlapHomologyEquivClock line 180