OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicSpace.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.PeriodicSpace.Torus line 11

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:700 (same declaration text).

  2. abbrev OAI.VelocityDetection.PeriodicSpace.compatible line 13
  3. def OAI.VelocityDetection.PeriodicSpace.cover line 15

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:702 (same declaration text).

  4. theorem OAI.VelocityDetection.PeriodicSpace.continuous_cover line 17
  5. theorem OAI.VelocityDetection.PeriodicSpace.cover_surjective line 22
  6. theorem OAI.VelocityDetection.PeriodicSpace.cover_add line 27
  7. theorem OAI.VelocityDetection.PeriodicSpace.cover_zero line 29
  8. def OAI.VelocityDetection.PeriodicSpace.realLift line 31
  9. theorem OAI.VelocityDetection.PeriodicSpace.realLift_apply line 36
  10. theorem OAI.VelocityDetection.PeriodicSpace.realLift_zero line 39
  11. theorem OAI.VelocityDetection.PeriodicSpace.realLift_add line 41
  12. theorem OAI.VelocityDetection.PeriodicSpace.realLift_neg line 44
  13. theorem OAI.VelocityDetection.PeriodicSpace.realLift_sub line 46
  14. theorem OAI.VelocityDetection.PeriodicSpace.realLift_smul line 49
  15. theorem OAI.VelocityDetection.PeriodicSpace.ext_fun line 52
  16. theorem OAI.VelocityDetection.PeriodicSpace.norm_realLift line 58
  17. def OAI.VelocityDetection.PeriodicSpace.realLiftLI line 68
  18. def OAI.VelocityDetection.PeriodicSpace.translate line 74
  19. theorem OAI.VelocityDetection.PeriodicSpace.translate_apply line 77
  20. theorem OAI.VelocityDetection.PeriodicSpace.translate_zero line 80
  21. theorem OAI.VelocityDetection.PeriodicSpace.translate_add line 85
  22. theorem OAI.VelocityDetection.PeriodicSpace.norm_translate_le line 91
  23. theorem OAI.VelocityDetection.PeriodicSpace.norm_translate line 97
  24. def OAI.VelocityDetection.PeriodicSpace.translateLI line 104
  25. theorem OAI.VelocityDetection.PeriodicSpace.continuous_translate line 110