OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorFluid.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit source program has a unique classical fluid realization. The force is fixed before choosing the scalar solution.

  1. def OAI.ForcedComputation.VelocityDetector.detectorForce line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorFluid_exists line 19