OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MildScalarSupportedData.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VelocityDetection.MildScalar.SupportedData line 17
  2. def OAI.VelocityDetection.MildScalar.SupportedData.jets line 37
  3. theorem OAI.VelocityDetection.MildScalar.SupportedData.jets_value line 40
  4. theorem OAI.VelocityDetection.MildScalar.SupportedData.continuous_jets line 43
  5. theorem OAI.VelocityDetection.MildScalar.SupportedData.restrict_jets line 46
  6. def OAI.VelocityDetection.MildScalar.SupportedData.curve line 50
  7. theorem OAI.VelocityDetection.MildScalar.SupportedData.curve_apply line 53
  8. theorem OAI.VelocityDetection.MildScalar.SupportedData.lower_curve line 56
  9. theorem OAI.VelocityDetection.MildScalar.SupportedData.short_curve line 62
  10. def OAI.VelocityDetection.MildScalar.finiteSolution line 81
  11. theorem OAI.VelocityDetection.MildScalar.lower_finiteSolution line 84
  12. theorem OAI.VelocityDetection.MildScalar.short_finiteSolution line 88
  13. theorem OAI.VelocityDetection.MildScalar.finiteSolution_agree line 94
  14. def OAI.VelocityDetection.MildScalar.globalJets line 105
  15. theorem OAI.VelocityDetection.MildScalar.globalJets_eq_finite line 109
  16. theorem OAI.VelocityDetection.MildScalar.restrict_globalJets line 117
  17. theorem OAI.VelocityDetection.MildScalar.continuousOn_globalJets line 122
  18. def OAI.VelocityDetection.MildScalar.scalar line 138
  19. theorem OAI.VelocityDetection.MildScalar.value_globalJets line 140
  20. theorem OAI.VelocityDetection.MildScalar.contDiff_scalar_space line 145