OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PeriodicLatticeCorollaryGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The exact label and open slab of the rapid torus corollary.

  1. def OAI.PeriodicLattice.RapidTorus.corollaryStart line 13
  2. def OAI.PeriodicLattice.RapidTorus.corollaryDetector line 14
  3. def OAI.PeriodicLattice.RapidTorus.pointTransform line 17
  4. theorem OAI.PeriodicLattice.RapidTorus.pointTransform_first line 20
  5. theorem OAI.PeriodicLattice.RapidTorus.pointTransform_second line 25
  6. theorem OAI.PeriodicLattice.RapidTorus.pointTransform_third line 28
  7. theorem OAI.PeriodicLattice.RapidTorus.pointTransform_initial line 31
  8. theorem OAI.PeriodicLattice.RapidTorus.corollaryDetector_open line 36
  9. theorem OAI.PeriodicLattice.RapidTorus.corollaryDetector_mem line 46
  10. theorem OAI.PeriodicLattice.RapidTorus.transformed_curve_event line 56
  11. theorem OAI.PeriodicLattice.RapidTorus.transformed_path_event line 98
  12. theorem OAI.PeriodicLattice.RapidTorus.velocity_shift_pointTransform line 105
  13. def OAI.PeriodicLattice.RapidTorus.corollaryPath line 117
  14. theorem OAI.PeriodicLattice.RapidTorus.corollaryPath_start line 119
  15. theorem OAI.PeriodicLattice.RapidTorus.corollaryPath_hasDerivAt line 122
  16. theorem OAI.PeriodicLattice.RapidTorus.corollaryPath_unique line 133