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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The detector force stays in one compact horizontal subset of the processor chart. Continuity supplies the boundary faces of the unit cell.

  1. def OAI.ForcedComputation.VelocityDetector.openUnitPlane line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.mem_openUnitPlane line 16
  3. theorem OAI.ForcedComputation.VelocityDetector.openUnitPlane_open line 20
  4. theorem OAI.ForcedComputation.VelocityDetector.threeAtLeastTwo line 23
  5. def OAI.ForcedComputation.VelocityDetector.injectionSupport line 25
  6. theorem OAI.ForcedComputation.VelocityDetector.injectionSupport_inside line 31
  7. theorem OAI.ForcedComputation.VelocityDetector.continuous_zero_on_unit_faces line 38
  8. theorem OAI.ForcedComputation.VelocityDetector.detectorForce_fixed_horizontal_support line 51
  9. theorem OAI.ForcedComputation.VelocityDetector.processor_detector_force_support line 97