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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A translation can be inserted at any sufficiently small rational scale inside the existing processor chart.

  1. def OAI.ForcedComputation.translationInstruction line 12
  2. theorem OAI.ForcedComputation.translationInstruction_image line 15
  3. theorem OAI.ForcedComputation.translationInstruction_singleton_valid line 22